From b663c658c80cee918afe37222e62dd1e5db33f5c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Oct 2013 14:22:36 -0500 Subject: Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity. Minor cleanup. --- src/smt/options | 2 +- src/smt/smt_engine.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/smt') diff --git a/src/smt/options b/src/smt/options index 7a72881b4..d2455b520 100644 --- a/src/smt/options +++ b/src/smt/options @@ -49,7 +49,7 @@ option repeatSimp --repeat-simp bool :read-write make multiple passes with nonclausal simplifier option sortInference --sort-inference bool :read-write :default false - apply sort inference to input problem + calculate sort inference of input problem, convert the input based on monotonic sorts common-option incrementalSolving incremental -i --incremental bool enable incremental solving diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d080ea6a..85a245a09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1979,7 +1979,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { } d_nonClausalLearnedLiterals.clear(); - + for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { Node cProp = (*pos).first.eqNode((*pos).second); Assert(d_topLevelSubstitutions.apply(cProp) == cProp); -- cgit v1.2.3