Home
last modified time | relevance | path

Searched refs:var_bound (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dsort_inference.cpp125 std::map<Node, Node> var_bound; in initialize() local
126 process(a, var_bound, visited); in initialize()
170 std::map<Node, Node> var_bound; in initialize() local
201 std::map<Node, Node> var_bound; in simplify() local
298 std::map<Node, Node> var_bound; in computeMonotonicity() local
385 var_bound[ n[0][i] ] = n; in process()
467 if( it!=var_bound.end() ){ in process()
515 var_bound[n[0][i]] = n; in processMonotonic()
528 if( var_bound.find( n[i] )!=var_bound.end() ){ in processMonotonic()
634 var_bound[ n[0][i] ] = v; in simplifyNode()
[all …]
H A Dsort_inference.h81 int process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited );
84 …void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map<…
98 std::map<Node, Node>& var_bound,
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Dbound_propagator.h166 typedef std::pair<var, bound *> var_bound; typedef
167 svector<var_bound> m_todo;
H A Dbound_propagator.cpp800 svector<var_bound> & todo = const_cast<bound_propagator*>(this)->m_todo; in explain()
803 todo.push_back(var_bound(x, b)); in explain()
806 var_bound & vb = todo[qhead]; in explain()
833 todo.push_back(var_bound(x_i, b)); in explain()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Dbound_propagator.h166 typedef std::pair<var, bound *> var_bound; typedef
167 svector<var_bound> m_todo;
H A Dbound_propagator.cpp800 svector<var_bound> & todo = const_cast<bound_propagator*>(this)->m_todo; in explain()
803 todo.push_back(var_bound(x, b)); in explain()
806 var_bound & vb = todo[qhead]; in explain()
833 todo.push_back(var_bound(x_i, b)); in explain()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/
H A Dinst_match_generator.cpp631 std::map< Node, bool > var_bound; in InstMatchGeneratorMultiLinear() local
645 if( var_bound.find( v )!=var_bound.end() ){ in InstMatchGeneratorMultiLinear()
665 var_bound[var_contains[mp][i]] = true; in InstMatchGeneratorMultiLinear()
/dports/math/z3/z3-z3-4.8.13/src/test/lp/
H A Dnla_solver_test.cpp23 svector<lpvar> get_monic(int monic_size, int var_bound, random_gen& rand) { in get_monic() argument
26 lpvar j = rand() % var_bound; in get_monic()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/lp/
H A Dnla_solver_test.cpp23 svector<lpvar> get_monic(int monic_size, int var_bound, random_gen& rand) {
26 lpvar j = rand() % var_bound;