From d0e61e49bf51ca7d67188dd71b5f27cd45f6f2ff Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 30 Apr 2018 15:33:21 -0500 Subject: Refactor real2int (#1813) This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. --- src/smt/smt_engine.cpp | 113 +++---------------------------------------------- 1 file changed, 6 insertions(+), 107 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55576870d..97e3f0215 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -73,6 +73,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -93,7 +94,6 @@ #include "smt_util/boolean_simplification.h" #include "smt_util/nary_builder.h" #include "smt_util/node_visitor.h" -#include "theory/arith/arith_msum.h" #include "theory/booleans/circuit_propagator.h" #include "theory/bv/bvintropow2.h" #include "theory/bv/theory_bv_rewriter.h" @@ -553,7 +553,7 @@ class SmtEnginePrivate : public NodeManagerListener { /** TODO: whether certain preprocess steps are necessary */ //bool d_needsExpandDefs; - + //------------------------------- expression names /** mapping from expressions to name */ context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames; @@ -2586,9 +2586,11 @@ void SmtEnginePrivate::finishInit() { std::unique_ptr intToBV(new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr pbProc( new PseudoBooleanProcessor(d_preprocessingPassContext.get())); - + std::unique_ptr realToInt( + new RealToInt(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); + d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); std::unique_ptr bvToBool( @@ -2759,97 +2761,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map NodeMap; -Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) { - Trace("real-as-int-debug") << "Convert : " << n << std::endl; - NodeMap::iterator find = cache.find(n); - if (find != cache.end()) { - return (*find).second; - }else{ - Node ret = n; - if( n.getNumChildren()>0 ){ - if( n.getKind()==kind::EQUAL || n.getKind()==kind::GEQ || n.getKind()==kind::LT || n.getKind()==kind::GT || n.getKind()==kind::LEQ ){ - ret = Rewriter::rewrite( n ); - Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl; - if( !ret.isConst() ){ - Node ret_lit = ret.getKind()==kind::NOT ? ret[0] : ret; - bool ret_pol = ret.getKind()!=kind::NOT; - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(ret_lit, msum)) - { - //get common coefficient - std::vector< Node > coeffs; - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - Node v = itm->first; - Node c = itm->second; - if( !c.isNull() ){ - Assert( c.isConst() ); - coeffs.push_back( NodeManager::currentNM()->mkConst( Rational( c.getConst().getDenominator() ) ) ); - } - } - Node cc = coeffs.empty() ? Node::null() : ( coeffs.size()==1 ? coeffs[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, coeffs ) ) ); - std::vector< Node > sum; - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - Node v = itm->first; - Node c = itm->second; - Node s; - if( c.isNull() ){ - c = cc.isNull() ? NodeManager::currentNM()->mkConst( Rational( 1 ) ) : cc; - }else{ - if( !cc.isNull() ){ - c = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, c, cc ) ); - } - } - Assert( c.getType().isInteger() ); - if( v.isNull() ){ - sum.push_back( c ); - }else{ - Node vv = realToInt( v, cache, var_eq ); - if( vv.getType().isInteger() ){ - sum.push_back( NodeManager::currentNM()->mkNode( kind::MULT, c, vv ) ); - }else{ - throw TypeCheckingException(v.toExpr(), string("Cannot translate to Int: ") + v.toString()); - } - } - } - Node sumt = sum.empty() ? NodeManager::currentNM()->mkConst( Rational( 0 ) ) : ( sum.size()==1 ? sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, sum ) ); - ret = NodeManager::currentNM()->mkNode( ret_lit.getKind(), sumt, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); - if( !ret_pol ){ - ret = ret.negate(); - } - Trace("real-as-int") << "Convert : " << std::endl; - Trace("real-as-int") << " " << n << std::endl; - Trace("real-as-int") << " " << ret << std::endl; - }else{ - throw TypeCheckingException(n.toExpr(), string("Cannot translate to Int: ") + n.toString()); - } - } - }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - }else{ - if( n.isVar() ){ - if( !n.getType().isInteger() ){ - ret = NodeManager::currentNM()->mkSkolem("__realToInt_var", NodeManager::currentNM()->integerType(), "Variable introduced in realToInt pass"); - var_eq.push_back( n.eqNode( ret ) ); - TheoryModel* m = d_smt.d_theoryEngine->getModel(); - m->addSubstitution(n,ret); - } - } - } - cache[n] = ret; - return ret; - } -} - Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) { if( beneathMult ){ NodeMap::iterator find = bcache.find(n); @@ -4100,19 +4011,7 @@ void SmtEnginePrivate::processAssertions() { } if (options::solveRealAsInt()) { - Chat() << "converting reals to ints..." << endl; - unordered_map cache; - std::vector< Node > var_eq; - for(unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq)); - } - /* - if( !var_eq.empty() ){ - unsigned lastIndex = d_assertions.size()-1; - var_eq.insert( var_eq.begin(), d_assertions[lastIndex] ); - d_assertions.replace(last_index, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) ); - } - */ + d_preprocessingPassRegistry.getPass("real-to-int")->apply(&d_assertions); } if (options::solveIntAsBV() > 0) -- cgit v1.2.3