summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am2
-rw-r--r--src/options/smt_options.toml2
-rw-r--r--src/preprocessing/passes/real_to_int.cpp202
-rw-r--r--src/preprocessing/passes/real_to_int.h52
-rw-r--r--src/smt/smt_engine.cpp113
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress1/arith/real2int-test.smt229
7 files changed, 293 insertions, 108 deletions
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 <string>
+
+#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<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<Rational>().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 = 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<Node> 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<Node, Node, NodeHashFunction> cache;
+ std::vector<Node> 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 <unordered_map>
+#include <vector>
+
+#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<Node, Node, NodeHashFunction>;
+
+class RealToInt : public PreprocessingPass
+{
+ public:
+ RealToInt(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ Node realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& 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> intToBV(new IntToBV(d_preprocessingPassContext.get()));
std::unique_ptr<PseudoBooleanProcessor> pbProc(
new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
-
+ std::unique_ptr<RealToInt> 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> bvToBool(
@@ -2759,97 +2761,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
typedef std::unordered_map<Node, Node, NodeHashFunction> 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<Rational>().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; i<n.getNumChildren(); i++ ){
- Node nc = realToInt( 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("__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<Node, Node, NodeHashFunction> 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback