parameters: (clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True)
return_statement: return h
docstring: Return a HerbrandModel with a "small" model of clauses.
  
      sorts_to_minimize is a list of sorts, and relations_to_minimize is
      a list of relations,
  
      The model minimization occurs in 2 ways:
  
      First, minimize universe size lexicographically according to the order of
      sorts_to_minimize.
  
      Second, minimize the number of positive entries in the relations
      according to the order of relations_to_minimize.
  
      The parameter final_cond can be a list of objects have the following interface:
  
          cond():  returns a final condition as a clauses object
          start(): called before starting
          sat(): called if sat, return True if should ignore result
          unsat() : called if unsat
          assume() : if returns true, assume rather than check
docstring_summary: Return a HerbrandModel with a "small" model of clauses.
docstring_tokens: Return a HerbrandModel with a small model of clauses .
function: def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True):
      """
      Return a HerbrandModel with a "small" model of clauses.
  
      sorts_to_minimize is a list of sorts, and relations_to_minimize is
      a list of relations,
  
      The model minimization occurs in 2 ways:
  
      First, minimize universe size lexicographically according to the order of
      sorts_to_minimize.
  
      Second, minimize the number of positive entries in the relations
      according to the order of relations_to_minimize.
  
      The parameter final_cond can be a list of objects have the following interface:
  
          cond():  returns a final condition as a clauses object
          start(): called before starting
          sat(): called if sat, return True if should ignore result
          unsat() : called if unsat
          assume() : if returns true, assume rather than check
  
      """
  
      if opt_show_vcs.get():
          print ''
          print "definitions:"
          for df in clauses.defs:
              print df
              print
          print "axioms:"
          for fmla in clauses.fmlas:
              print fmla
              print
  
      s = z3.Solver()
      the_fmla = clauses_to_z3(clauses)
  #    iu.dbg('the_fmla')
      s.add(the_fmla)
      
      # res = decide(s)
      # if res == z3.unsat:
      #     return None
  
      assumes = []
      if final_cond is not None:
          if isinstance(final_cond,list):
              res = z3.unsat
              for fc in final_cond:
                  if not opt_incremental.get():
                      s = z3.Solver()
                      s.add(clauses_to_z3(clauses))
                      for fmla in assumes:
                          s.add(clauses_to_z3(fmla))
                  fc.start()
                  if fc.assume():
                      if opt_show_vcs.get():
                          print '\nassume: {}'.format(fc.cond())
                      s.add(clauses_to_z3(fc.cond()))
                      assumes.append(fc.cond())
                  else:
                      if opt_incremental.get():
                          s.push()
                      foo = fc.cond()
                      if opt_show_vcs.get():
                          print '\nassert: {}'.format(foo)
                      the_fmla = clauses_to_z3(foo)
  #                    iu.dbg('the_fmla')
                      s.add(the_fmla)
                      res = decide(s)
                      if res != z3.unsat:
                          if fc.sat():
                              res = z3.unsat
                          else:
                              break
                      else:
                          fc.unsat()
                      if opt_incremental.get():
                          s.pop()
          else:
              s.add(clauses_to_z3(final_cond))
              res = decide(s)
      else:
          res = decide(s)
      if res == z3.unsat:
          return None
  
      if shrink:
          print "searching for a small model...",
          sys.stdout.flush()
          for x in chain(sorts_to_minimize, relations_to_minimize):
              for n in itertools.count(1):
                  s.push()
                  sc = size_constraint(x, n)
                  s.add(formula_to_z3(sc))
                  res = decide(s)
                  if res == z3.sat:
                      break
                  else:
                      s.pop()
          print "done"
      m = get_model(s)
  #    print "model = {}".format(m)
  #    f = open("ivy.smt2","w")
  #    f.write(s.to_smt2())
  #    f.close()
      h = HerbrandModel(s,m,used_symbols_clauses(clauses))
      return h
function_tokens: def get_small_model ( clauses , sorts_to_minimize , relations_to_minimize , final_cond = None , shrink = True ) : if opt_show_vcs . get ( ) : print '' print "definitions:" for df in clauses . defs : print df print print "axioms:" for fmla in clauses . fmlas : print fmla print s = z3 . Solver ( ) the_fmla = clauses_to_z3 ( clauses ) #    iu.dbg('the_fmla') s . add ( the_fmla ) # res = decide(s) # if res == z3.unsat: #     return None assumes = [ ] if final_cond is not None : if isinstance ( final_cond , list ) : res = z3 . unsat for fc in final_cond : if not opt_incremental . get ( ) : s = z3 . Solver ( ) s . add ( clauses_to_z3 ( clauses ) ) for fmla in assumes : s . add ( clauses_to_z3 ( fmla ) ) fc . start ( ) if fc . assume ( ) : if opt_show_vcs . get ( ) : print '\nassume: {}' . format ( fc . cond ( ) ) s . add ( clauses_to_z3 ( fc . cond ( ) ) ) assumes . append ( fc . cond ( ) ) else : if opt_incremental . get ( ) : s . push ( ) foo = fc . cond ( ) if opt_show_vcs . get ( ) : print '\nassert: {}' . format ( foo ) the_fmla = clauses_to_z3 ( foo ) #                    iu.dbg('the_fmla') s . add ( the_fmla ) res = decide ( s ) if res != z3 . unsat : if fc . sat ( ) : res = z3 . unsat else : break else : fc . unsat ( ) if opt_incremental . get ( ) : s . pop ( ) else : s . add ( clauses_to_z3 ( final_cond ) ) res = decide ( s ) else : res = decide ( s ) if res == z3 . unsat : return None if shrink : print "searching for a small model..." , sys . stdout . flush ( ) for x in chain ( sorts_to_minimize , relations_to_minimize ) : for n in itertools . count ( 1 ) : s . push ( ) sc = size_constraint ( x , n ) s . add ( formula_to_z3 ( sc ) ) res = decide ( s ) if res == z3 . sat : break else : s . pop ( ) print "done" m = get_model ( s ) #    print "model = {}".format(m) #    f = open("ivy.smt2","w") #    f.write(s.to_smt2()) #    f.close() h = HerbrandModel ( s , m , used_symbols_clauses ( clauses ) ) return h