diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-30 10:14:32 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-30 10:14:42 -0500 |
| commit | 0c2eafec69b694a507ac914bf285fe0574be085f (patch) | |
| tree | 0f3601964ee8f883c93d506f1f0476e5888936ae /src/theory/uf | |
| parent | 546e6aca016ea1f9b7da0bcfda5bed833a7a13ec (diff) | |
Bug fixes and improvements for symmetry breaking, it now supports multiple sorts. Working on monotonicity inference.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 82cd1f809..163dd3c1f 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -120,8 +120,7 @@ void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){ d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null()); } if( options::ufssSymBreak() ){ - //d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); - d_cf->d_thss->getSymmetryBreaker()->queueFact( a.eqNode( n ).negate() ); + d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); } } setDisequal( b, n, t, false ); @@ -527,8 +526,7 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ d_thss->getDisequalityPropagator()->merge(a, b); } if( options::ufssSymBreak() ){ - //d_thss->getSymmetryBreaker()->merge(a, b); - d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ) ); + d_thss->getSymmetryBreaker()->merge(a, b); } } } @@ -583,8 +581,7 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null()); } if( options::ufssSymBreak() ){ - //d_thss->getSymmetryBreaker()->assertDisequal(a, b); - d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ).negate() ); + d_thss->getSymmetryBreaker()->assertDisequal(a, b); } } } @@ -1478,8 +1475,7 @@ void StrongSolverTheoryUF::newEqClass( Node n ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << n << " : " << n.getType() << std::endl; c->newEqClass( n ); if( options::ufssSymBreak() ){ - //d_sym_break->newEqClass( n ); - d_sym_break->queueFact( n ); + d_sym_break->newEqClass( n ); } } } |