From d0e61e49bf51ca7d67188dd71b5f27cd45f6f2ff Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 30 Apr 2018 15:33:21 -0500 Subject: [PATCH] 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/Makefile.am | 2 + src/options/smt_options.toml | 2 +- src/preprocessing/passes/real_to_int.cpp | 202 ++++++++++++++++++ src/preprocessing/passes/real_to_int.h | 52 +++++ src/smt/smt_engine.cpp | 113 +--------- test/regress/Makefile.tests | 1 + .../regress/regress1/arith/real2int-test.smt2 | 29 +++ 7 files changed, 293 insertions(+), 108 deletions(-) create mode 100644 src/preprocessing/passes/real_to_int.cpp create mode 100644 src/preprocessing/passes/real_to_int.h create mode 100644 test/regress/regress1/arith/real2int-test.smt2 diff --git a/src/Makefile.am b/src/Makefile.am index 886cd1af9..e9fcb5913 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -72,6 +72,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bool_to_bv.h \ preprocessing/passes/bv_to_bool.cpp \ preprocessing/passes/bv_to_bool.h \ + preprocessing/passes/real_to_int.cpp \ + preprocessing/passes/real_to_int.h \ preprocessing/passes/symmetry_detect.cpp \ preprocessing/passes/symmetry_detect.h \ preprocessing/preprocessing_pass.cpp \ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index e7a385a42..73cb87dd4 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -622,4 +622,4 @@ header = "options/smt_options.h" type = "bool" default = "false" read_only = true - help = "attempt to solve a pure real satisfiable problem as a integer problem (for non-linear)" + help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp new file mode 100644 index 000000000..c92f4b962 --- /dev/null +++ b/src/preprocessing/passes/real_to_int.cpp @@ -0,0 +1,202 @@ +/********************* */ +/*! \file real_to_int.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The RealToInt preprocessing pass + ** + ** Converts real operations into integer operations + **/ + +#include "preprocessing/passes/real_to_int.h" + +#include + +#include "theory/arith/arith_msum.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& 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 msum; + if (ArithMSum::getMonomialSumLit(ret_lit, msum)) + { + // get common coefficient + std::vector coeffs; + for (std::map::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 sum; + for (std::map::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 = realToIntInternal(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 children; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + Node nc = realToIntInternal(n[i], cache, var_eq); + childChanged = childChanged || nc != n[i]; + children.push_back(nc); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + } + } + } + else + { + if (n.isVar()) + { + if (!n.getType().isInteger()) + { + ret = NodeManager::currentNM()->mkSkolem( + "__realToIntInternal_var", + NodeManager::currentNM()->integerType(), + "Variable introduced in realToIntInternal pass"); + var_eq.push_back(n.eqNode(ret)); + TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel(); + m->addSubstitution(n, ret); + } + } + } + cache[n] = ret; + return ret; + } +} + +RealToInt::RealToInt(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "real-to-int"){}; + +PreprocessingPassResult RealToInt::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + unordered_map cache; + std::vector var_eq; + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace( + i, realToIntInternal((*assertionsToPreprocess)[i], cache, var_eq)); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h new file mode 100644 index 000000000..eb4ac6593 --- /dev/null +++ b/src/preprocessing/passes/real_to_int.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file real_to_int.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The RealToInt preprocessing pass + ** + ** Converts real operations into integer operations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#define __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H + +#include +#include + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map; + +class RealToInt : public PreprocessingPass +{ + public: + RealToInt(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node realToIntInternal(TNode n, NodeMap& cache, std::vector& var_eq); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ 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) diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index f799c20d5..f8a32046f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -998,6 +998,7 @@ REG1_TESTS = \ regress1/arith/mult.02.smt2 \ regress1/arith/pbrewrites-test.smt2 \ regress1/arith/problem__003.smt2 \ + regress1/arith/real2int-test.smt2 \ regress1/arrayinuf_error.smt2 \ regress1/aufbv/bug580.smt2 \ regress1/aufbv/fuzz10.smt \ diff --git a/test/regress/regress1/arith/real2int-test.smt2 b/test/regress/regress1/arith/real2int-test.smt2 new file mode 100644 index 000000000..77bc1eda2 --- /dev/null +++ b/test/regress/regress1/arith/real2int-test.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --solve-real-as-int +; EXPECT: sat +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoS3 () Real) +(declare-fun skoSX () Real) +(assert (and (not (<= (* skoX (+ (+ (* skoS3 (/ 471 100)) (* skoSX (/ 157 100))) (* skoX (* skoS3 (- 8))))) (+ (* skoS3 3) skoSX))) (and (not (<= skoX 0)) (and (not (<= skoSX 0)) (not (<= skoS3 0)))))) +(check-sat) +(exit) -- 2.30.2