addOperator(kind::SINE, "sin");
addOperator(kind::COSINE, "cos");
addOperator(kind::TANGENT, "tan");
+ addOperator(kind::COSECANT, "csc");
+ addOperator(kind::SECANT, "sec");
+ addOperator(kind::COTANGENT, "cot");
+ addOperator(kind::ARCSINE, "arcsin");
+ addOperator(kind::ARCCOSINE, "arccos");
+ addOperator(kind::ARCTANGENT, "arctan");
+ addOperator(kind::ARCCOSECANT, "arccsc");
+ addOperator(kind::ARCSECANT, "arcsec");
+ addOperator(kind::ARCCOTANGENT, "arccot");
+
+ addOperator(kind::SQRT, "sqrt");
}
void Smt2::addBitvectorOperators() {
case kind::SINE:
case kind::COSINE:
case kind::TANGENT:
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT:
+ case kind::SQRT:
case kind::MINUS:
case kind::UMINUS:
case kind::LT:
case kind::SINE: return "sin";
case kind::COSINE: return "cos";
case kind::TANGENT: return "tan";
+ case kind::COSECANT: return "csc";
+ case kind::SECANT: return "sec";
+ case kind::COTANGENT: return "cot";
+ case kind::ARCSINE: return "arcsin";
+ case kind::ARCCOSINE: return "arccos";
+ case kind::ARCTANGENT: return "arctan";
+ case kind::ARCCOSECANT: return "arccsc";
+ case kind::ARCSECANT: return "arcsec";
+ case kind::ARCCOTANGENT: return "arccot";
+ case kind::SQRT: return "sqrt";
case kind::MINUS: return "-";
case kind::UMINUS: return "-";
case kind::LT: return "<";
case kind::SINE:
case kind::COSINE:
case kind::TANGENT:
- return preRewriteTranscendental(t);
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT: return preRewriteTranscendental(t);
case kind::INTS_DIVISION:
case kind::INTS_MODULUS:
return RewriteResponse(REWRITE_DONE, t);
case kind::SINE:
case kind::COSINE:
case kind::TANGENT:
- return postRewriteTranscendental(t);
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT: return postRewriteTranscendental(t);
case kind::INTS_DIVISION:
case kind::INTS_MODULUS:
return RewriteResponse(REWRITE_DONE, t);
RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
Trace("arith-tf-rewrite") << "Rewrite transcendental function : " << t << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
switch( t.getKind() ){
case kind::EXPONENTIAL: {
if(t[0].getKind() == kind::CONST_RATIONAL){
- Node one = NodeManager::currentNM()->mkConst(Rational(1));
+ Node one = nm->mkConst(Rational(1));
if(t[0].getConst<Rational>().sgn()>=0 && t[0].getType().isInteger() && t[0]!=one){
- return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::POW, NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, one ), t[0]));
+ return RewriteResponse(
+ REWRITE_AGAIN,
+ nm->mkNode(kind::POW, nm->mkNode(kind::EXPONENTIAL, one), t[0]));
}else{
return RewriteResponse(REWRITE_DONE, t);
}
}else if(t[0].getKind() == kind::PLUS ){
std::vector<Node> product;
for( unsigned i=0; i<t[0].getNumChildren(); i++ ){
- product.push_back( NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, t[0][i] ) );
+ product.push_back(nm->mkNode(kind::EXPONENTIAL, t[0][i]));
}
- return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::MULT, product));
+ return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::MULT, product));
}
}
break;
case kind::SINE:
if(t[0].getKind() == kind::CONST_RATIONAL){
const Rational& rat = t[0].getConst<Rational>();
- NodeManager* nm = NodeManager::currentNM();
if(rat.sgn() == 0){
return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(0)));
}
if (r_abs > rone)
{
//add/substract 2*pi beyond scope
- Node ra_div_two = NodeManager::currentNM()->mkNode(
+ Node ra_div_two = nm->mkNode(
kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo);
Node new_pi_factor;
if( r.sgn()==1 ){
- new_pi_factor = NodeManager::currentNM()->mkNode( kind::MINUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) );
+ new_pi_factor =
+ nm->mkNode(kind::MINUS,
+ pi_factor,
+ nm->mkNode(kind::MULT, ntwo, ra_div_two));
}else{
Assert( r.sgn()==-1 );
- new_pi_factor = NodeManager::currentNM()->mkNode( kind::PLUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) );
+ new_pi_factor =
+ nm->mkNode(kind::PLUS,
+ pi_factor,
+ nm->mkNode(kind::MULT, ntwo, ra_div_two));
}
- Node new_arg =
- NodeManager::currentNM()->mkNode(kind::MULT, new_pi_factor, pi);
+ Node new_arg = nm->mkNode(kind::MULT, new_pi_factor, pi);
if (!rem.isNull())
{
- new_arg =
- NodeManager::currentNM()->mkNode(kind::PLUS, new_arg, rem);
+ new_arg = nm->mkNode(kind::PLUS, new_arg, rem);
}
// sin( 2*n*PI + x ) = sin( x )
- return RewriteResponse(
- REWRITE_AGAIN_FULL,
- NodeManager::currentNM()->mkNode(kind::SINE, new_arg));
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::SINE, new_arg));
}
else if (r_abs == rone)
{
{
return RewriteResponse(
REWRITE_AGAIN_FULL,
- NodeManager::currentNM()->mkNode(
- kind::UMINUS,
- NodeManager::currentNM()->mkNode(kind::SINE, rem)));
+ nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, rem)));
}
}
else if (rem.isNull())
}
break;
case kind::COSINE: {
- return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE,
- NodeManager::currentNM()->mkNode( kind::MINUS,
- NodeManager::currentNM()->mkNode( kind::MULT,
- NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ),
- NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ),
- t[0] ) ) );
- } break;
+ return RewriteResponse(
+ REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::SINE,
+ nm->mkNode(kind::MINUS,
+ nm->mkNode(kind::MULT,
+ nm->mkConst(Rational(1) / Rational(2)),
+ mkPi()),
+ t[0])));
+ }
+ break;
case kind::TANGENT:
- return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode(kind::DIVISION, NodeManager::currentNM()->mkNode( kind::SINE, t[0] ),
- NodeManager::currentNM()->mkNode( kind::COSINE, t[0] ) ));
+ {
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::DIVISION,
+ nm->mkNode(kind::SINE, t[0]),
+ nm->mkNode(kind::COSINE, t[0])));
+ }
+ break;
+ case kind::COSECANT:
+ {
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::DIVISION,
+ mkRationalNode(Rational(1)),
+ nm->mkNode(kind::SINE, t[0])));
+ }
+ break;
+ case kind::SECANT:
+ {
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::DIVISION,
+ mkRationalNode(Rational(1)),
+ nm->mkNode(kind::COSINE, t[0])));
+ }
+ break;
+ case kind::COTANGENT:
+ {
+ return RewriteResponse(REWRITE_AGAIN_FULL,
+ nm->mkNode(kind::DIVISION,
+ nm->mkNode(kind::COSINE, t[0]),
+ nm->mkNode(kind::SINE, t[0])));
+ }
+ break;
default:
break;
}
operator SINE 1 "sine"
operator COSINE 1 "consine"
operator TANGENT 1 "tangent"
+operator COSECANT 1 "cosecant"
+operator SECANT 1 "secant"
+operator COTANGENT 1 "cotangent"
+operator ARCSINE 1 "arc sine"
+operator ARCCOSINE 1 "arc consine"
+operator ARCTANGENT 1 "arc tangent"
+operator ARCCOSECANT 1 "arc cosecant"
+operator ARCSECANT 1 "arc secant"
+operator ARCCOTANGENT 1 "arc cotangent"
+
+operator SQRT 1 "square root"
constant DIVISIBLE_OP \
::CVC4::Divisible \
typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
+
+typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule
nullaryoperator PI "pi"
NonlinearExtension::NonlinearExtension(TheoryArith& containing,
eq::EqualityEngine* ee)
- : d_lemmas(containing.getUserContext()),
+ : d_def_lemmas(containing.getUserContext()),
+ d_lemmas(containing.getUserContext()),
d_zero_split(containing.getUserContext()),
d_skolem_atoms(containing.getUserContext()),
d_containing(containing),
d_ee(ee),
- d_needsLastCall(false) {
+ d_needsLastCall(false)
+{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
}
bool NonlinearExtension::isTranscendentalKind(Kind k) {
- Assert(k != TANGENT && k != COSINE); // eliminated
+ // many operators are eliminated during rewriting
+ Assert(k != TANGENT && k != COSINE && k != COSECANT && k != SECANT
+ && k != COTANGENT);
return k == EXPONENTIAL || k == SINE || k == PI;
}
if (check_assertions.empty())
{
+ Trace("nl-ext-tf-check-model") << "...simple check succeeded." << std::endl;
return true;
}
else
{
+ Trace("nl-ext-tf-check-model") << "...simple check failed." << std::endl;
// TODO (#1450) check model for general case
return false;
}
return comp == d_true;
}
}
-
Trace("nl-ext-tf-check-model-simple") << " failed due to unknown literal."
<< std::endl;
return false;
d_tf_check_model_bounds.clear();
int lemmas_proc = 0;
- std::vector<Node> lemmas;
-
+ std::vector<Node> lemmas;
+ NodeManager* nm = NodeManager::currentNM();
+
Trace("nl-ext-mv") << "Extended terms : " << std::endl;
// register the extended function terms
std::map< Node, Node > mvarg_to_term;
+ std::vector<Node> trig_no_base;
for( unsigned i=0; i<xts.size(); i++ ){
Node a = xts[i];
computeModelValue(a, 0);
{
if( d_trig_is_base.find( a )==d_trig_is_base.end() ){
consider = false;
- if( d_trig_base.find( a )==d_trig_base.end() ){
- Node y = NodeManager::currentNM()->mkSkolem("y",NodeManager::currentNM()->realType(),"phase shifted trigonometric arg");
- Node new_a = NodeManager::currentNM()->mkNode( a.getKind(), y );
- d_trig_is_base[new_a] = true;
- d_trig_base[a] = new_a;
- Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
- if( d_pi.isNull() ){
- mkPi();
- getCurrentPiBounds( lemmas );
- }
- Node shift = NodeManager::currentNM()->mkSkolem( "s", NodeManager::currentNM()->integerType(), "number of shifts" );
- // FIXME : do not introduce shift here, instead needs model-based
- // refinement for constant shifts (#1284)
- Node shift_lem = NodeManager::currentNM()->mkNode(
- AND,
- mkValidPhase(y, d_pi),
- a[0].eqNode(NodeManager::currentNM()->mkNode(
- PLUS,
- y,
- NodeManager::currentNM()->mkNode(
- MULT,
- NodeManager::currentNM()->mkConst(Rational(2)),
- shift,
- d_pi))),
- // particular case of above for shift=0
- NodeManager::currentNM()->mkNode(
- IMPLIES, mkValidPhase(a[0], d_pi), a[0].eqNode(y)),
- new_a.eqNode(a));
- //must do preprocess on this one
- Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl;
- d_containing.getOutputChannel().lemma(shift_lem, false, true);
- lemmas_proc++;
+ trig_no_base.push_back(a);
+ if (d_pi.isNull())
+ {
+ mkPi();
+ getCurrentPiBounds(lemmas);
}
}
}
//verify they have the same model value
if( d_mv[1][a]!=d_mv[1][itrm->second] ){
// if not, add congruence lemma
- Node cong_lemma = NodeManager::currentNM()->mkNode(
+ Node cong_lemma = nm->mkNode(
IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second));
lemmas.push_back( cong_lemma );
//Assert( false );
return lemmas_proc;
}
+ // process SINE phase shifting
+ for (const Node& a : trig_no_base)
+ {
+ if (d_trig_base.find(a) == d_trig_base.end())
+ {
+ Node y =
+ nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+ Node new_a = nm->mkNode(a.getKind(), y);
+ d_trig_is_base[new_a] = true;
+ d_trig_base[a] = new_a;
+ Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
+ << std::endl;
+ Assert(!d_pi.isNull());
+ Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+ // FIXME : do not introduce shift here, instead needs model-based
+ // refinement for constant shifts (#1284)
+ Node shift_lem = nm->mkNode(
+ AND,
+ mkValidPhase(y, d_pi),
+ a[0].eqNode(nm->mkNode(
+ PLUS,
+ y,
+ nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi))),
+ // particular case of above for shift=0
+ nm->mkNode(IMPLIES, mkValidPhase(a[0], d_pi), a[0].eqNode(y)),
+ new_a.eqNode(a));
+ // must do preprocess on this one
+ Trace("nl-ext-lemma")
+ << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl;
+ d_containing.getOutputChannel().lemma(shift_lem, false, true);
+ lemmas_proc++;
+ }
+ }
+ if (lemmas_proc > 0)
+ {
+ Trace("nl-ext") << " ...finished with " << lemmas_proc
+ << " new lemmas SINE phase shifting." << std::endl;
+ return lemmas_proc;
+ }
// register constants
registerMonomial(d_one);
}
}
+void NonlinearExtension::addDefinition(Node lem)
+{
+ Trace("nl-ext") << "NonlinearExtension::addDefinition : " << lem << std::endl;
+ d_def_lemmas.insert(lem);
+}
+
+void NonlinearExtension::presolve()
+{
+ Trace("nl-ext") << "NonlinearExtension::presolve, #defs = "
+ << d_def_lemmas.size() << std::endl;
+ for (NodeSet::const_iterator it = d_def_lemmas.begin();
+ it != d_def_lemmas.end();
+ ++it)
+ {
+ flushLemma(*it);
+ }
+}
+
void NonlinearExtension::assignOrderIds(std::vector<Node>& vars,
NodeMultiset& order,
unsigned orderType) {
antec.size() == 1 ? antec[0] : nm->mkNode(AND, antec);
lem = nm->mkNode(IMPLIES, antec_n, lem);
}
+ Trace("nl-ext-tf-tplanes-debug")
+ << "*** Tangent plane lemma (pre-rewrite): " << lem
+ << std::endl;
+ lem = Rewriter::rewrite(lem);
Trace("nl-ext-tf-tplanes") << "*** Tangent plane lemma : " << lem
<< std::endl;
// Figure 3 : line 9
nm->mkNode(GEQ, tf[0], s == 0 ? bounds[s] : c),
nm->mkNode(LEQ, tf[0], s == 0 ? c : bounds[s]));
lem = nm->mkNode(IMPLIES, antec_n, lem);
+ Trace("nl-ext-tf-tplanes-debug")
+ << "*** Secant plane lemma (pre-rewrite) : " << lem
+ << std::endl;
+ lem = Rewriter::rewrite(lem);
Trace("nl-ext-tf-tplanes") << "*** Secant plane lemma : " << lem
<< std::endl;
// Figure 3 : line 22
void check(Theory::Effort e);
/** Does this class need a call to check(...) at last call effort? */
bool needsCheckLastEffort() const { return d_needsLastCall; }
+ /** add definition
+ *
+ * This function notifies this class that lem is a formula that defines or
+ * constrains an auxiliary variable. For example, during
+ * TheoryArith::expandDefinitions, we replace a term like arcsin( x ) with an
+ * auxiliary variable k. The lemmas 0 <= k < pi and sin( x ) = k are added as
+ * definitions to this class.
+ */
+ void addDefinition(Node lem);
+ /** presolve
+ *
+ * This function is called during TheoryArith's presolve command.
+ * In this function, we send lemmas we accumulated during preprocessing,
+ * for instance, definitional lemmas from expandDefinitions are sent out
+ * on the output channel of TheoryArith in this function.
+ */
+ void presolve();
/** Compare arithmetic terms i and j based an ordering.
*
* orderType = 0 : compare concrete model values
// ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
std::map<Node, std::map<Node, Node> > d_mono_diff;
- // cache of all lemmas sent
+ /** cache of definition lemmas (user-context-dependent) */
+ NodeSet d_def_lemmas;
+ /** cache of all lemmas sent on the output channel (user-context-dependent) */
NodeSet d_lemmas;
+ /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
NodeSet d_zero_split;
// literals with Skolems (need not be satisfied by model)
case kind::SINE:
case kind::COSINE:
case kind::TANGENT:
- return Polynomial::isMember(n[0]);
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT:
+ case kind::SQRT: return Polynomial::isMember(n[0]);
case kind::PI:
return true;
default:
case kind::SINE:
case kind::COSINE:
case kind::TANGENT:
+ case kind::COSECANT:
+ case kind::SECANT:
+ case kind::COTANGENT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT:
+ case kind::SQRT:
case kind::PI:
return isTranscendentalMember(n);
case kind::ABS:
getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
getExtTheory()->addFunctionKind(kind::SINE);
- getExtTheory()->addFunctionKind(kind::COSINE);
- getExtTheory()->addFunctionKind(kind::TANGENT);
getExtTheory()->addFunctionKind(kind::PI);
}
}
static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
-
-TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- d_containing(containing),
- d_nlIncomplete( false),
- d_rowTracking(),
- d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
- d_qflraStatus(Result::SAT_UNKNOWN),
- d_unknownsInARow(0),
- d_hasDoneWorkSinceCut(false),
- d_learner(u),
- d_assertionsThatDoNotMatchTheirLiterals(c),
- d_nextIntegerCheckVar(0),
- d_constantIntegerVariables(c),
- d_diseqQueue(c, false),
- d_currentPropagationList(),
- d_learnedBounds(c),
- d_partialModel(c, DeltaComputeCallback(*this)),
- d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
- d_tableau(),
- d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
- d_diosolver(c),
- d_restartsCounter(0),
- d_tableauSizeHasBeenModified(false),
- d_tableauResetDensity(1.6),
- d_tableauResetPeriod(10),
- d_conflicts(c),
- d_blackBoxConflict(c, Node::null()),
- d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this)),
- d_cmEnabled(c, true),
-
- d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
- d_nonlinearExtension( NULL ),
- d_pass1SDP(NULL),
- d_otherSDP(NULL),
- d_lastContextIntegerAttempted(c,-1),
-
-
- d_DELTA_ZERO(0),
- d_approxCuts(c),
- d_fullCheckCounter(0),
- d_cutCount(c, 0),
- d_cutInContext(c),
- d_likelyIntegerInfeasible(c, false),
- d_guessedCoeffSet(c, false),
- d_guessedCoeffs(),
- d_treeLog(NULL),
- d_replayVariables(),
- d_replayConstraints(),
- d_lhsTmp(),
- d_approxStats(NULL),
- d_attemptSolveIntTurnedOff(u, 0),
- d_dioSolveResources(0),
- d_solveIntMaybeHelp(0u),
- d_solveIntAttempts(0u),
- d_statistics(),
- d_to_int_skolem(u),
- d_div_skolem(u),
- d_int_div_skolem(u)
+TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
+ context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo)
+ : d_containing(containing),
+ d_nlIncomplete(false),
+ d_rowTracking(),
+ d_constraintDatabase(
+ c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
+ d_qflraStatus(Result::SAT_UNKNOWN),
+ d_unknownsInARow(0),
+ d_hasDoneWorkSinceCut(false),
+ d_learner(u),
+ d_assertionsThatDoNotMatchTheirLiterals(c),
+ d_nextIntegerCheckVar(0),
+ d_constantIntegerVariables(c),
+ d_diseqQueue(c, false),
+ d_currentPropagationList(),
+ d_learnedBounds(c),
+ d_partialModel(c, DeltaComputeCallback(*this)),
+ d_errorSet(
+ d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
+ d_tableau(),
+ d_linEq(d_partialModel,
+ d_tableau,
+ d_rowTracking,
+ BasicVarModelUpdateCallBack(*this)),
+ d_diosolver(c),
+ d_restartsCounter(0),
+ d_tableauSizeHasBeenModified(false),
+ d_tableauResetDensity(1.6),
+ d_tableauResetPeriod(10),
+ d_conflicts(c),
+ d_blackBoxConflict(c, Node::null()),
+ d_congruenceManager(c,
+ d_constraintDatabase,
+ SetupLiteralCallBack(*this),
+ d_partialModel,
+ RaiseEqualityEngineConflict(*this)),
+ d_cmEnabled(c, true),
+
+ d_dualSimplex(
+ d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_fcSimplex(
+ d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_soiSimplex(
+ d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_attemptSolSimplex(
+ d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+ d_nonlinearExtension(NULL),
+ d_pass1SDP(NULL),
+ d_otherSDP(NULL),
+ d_lastContextIntegerAttempted(c, -1),
+
+ d_DELTA_ZERO(0),
+ d_approxCuts(c),
+ d_fullCheckCounter(0),
+ d_cutCount(c, 0),
+ d_cutInContext(c),
+ d_likelyIntegerInfeasible(c, false),
+ d_guessedCoeffSet(c, false),
+ d_guessedCoeffs(),
+ d_treeLog(NULL),
+ d_replayVariables(),
+ d_replayConstraints(),
+ d_lhsTmp(),
+ d_approxStats(NULL),
+ d_attemptSolveIntTurnedOff(u, 0),
+ d_dioSolveResources(0),
+ d_solveIntMaybeHelp(0u),
+ d_solveIntAttempts(0u),
+ d_statistics(),
+ d_to_int_skolem(u),
+ d_div_skolem(u),
+ d_int_div_skolem(u),
+ d_nlin_inverse_skolem(u)
{
if( options::nlExt() ){
d_nonlinearExtension = new NonlinearExtension(
Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
outputLemma(lem);
}
+
+ if (options::nlExt())
+ {
+ d_nonlinearExtension->presolve();
+ }
}
EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) {
Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
NodeManager* nm = NodeManager::currentNM();
- // eliminate here since involves division
- if( node.getKind()==kind::TANGENT ){
- node = nm->mkNode(kind::DIVISION, nm->mkNode( kind::SINE, node[0] ),
- nm->mkNode( kind::COSINE, node[0] ) );
+ // eliminate here since the rewritten form of these may introduce division
+ Kind k = node.getKind();
+ if (k == kind::TANGENT || k == kind::COSECANT || k == kind::SECANT
+ || k == kind::COTANGENT)
+ {
+ node = Rewriter::rewrite(node);
+ k = node.getKind();
}
- switch(node.getKind()) {
- case kind::DIVISION: {
- TNode num = node[0], den = node[1];
- Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den);
- if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+ switch (k)
+ {
+ case kind::DIVISION:
{
- // partial function: division
- if (d_divByZero.isNull())
+ TNode num = node[0], den = node[1];
+ Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den);
+ if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
- d_divByZero =
- nm->mkSkolem("divByZero",
- nm->mkFunctionType(nm->realType(), nm->realType()),
- "partial real division",
- NodeManager::SKOLEM_EXACT_NAME);
- logicRequest.widenLogic(THEORY_UF);
+ // partial function: division
+ if (d_divByZero.isNull())
+ {
+ d_divByZero =
+ nm->mkSkolem("divByZero",
+ nm->mkFunctionType(nm->realType(), nm->realType()),
+ "partial real division",
+ NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
+ ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
}
- Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
- ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
+ return ret;
+ break;
}
- return ret;
- break;
- }
- case kind::INTS_DIVISION: {
- // partial function: integer div
- TNode num = node[0], den = node[1];
- Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
- if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+ case kind::INTS_DIVISION:
{
- if (d_intDivByZero.isNull())
+ // partial function: integer div
+ TNode num = node[0], den = node[1];
+ Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
+ if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
- d_intDivByZero = nm->mkSkolem(
- "intDivByZero",
- nm->mkFunctionType(nm->integerType(), nm->integerType()),
- "partial integer division",
- NodeManager::SKOLEM_EXACT_NAME);
- logicRequest.widenLogic(THEORY_UF);
+ if (d_intDivByZero.isNull())
+ {
+ d_intDivByZero = nm->mkSkolem(
+ "intDivByZero",
+ nm->mkFunctionType(nm->integerType(), nm->integerType()),
+ "partial integer division",
+ NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
+ ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
}
- Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
- ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
+ return ret;
+ break;
}
- return ret;
- break;
- }
- case kind::INTS_MODULUS: {
- // partial function: mod
- TNode num = node[0], den = node[1];
- Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
- if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
+ case kind::INTS_MODULUS:
{
- if (d_modZero.isNull())
+ // partial function: mod
+ TNode num = node[0], den = node[1];
+ Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
+ if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
- d_modZero = nm->mkSkolem(
- "modZero",
- nm->mkFunctionType(nm->integerType(), nm->integerType()),
- "partial modulus",
- NodeManager::SKOLEM_EXACT_NAME);
- logicRequest.widenLogic(THEORY_UF);
+ if (d_modZero.isNull())
+ {
+ d_modZero = nm->mkSkolem(
+ "modZero",
+ nm->mkFunctionType(nm->integerType(), nm->integerType()),
+ "partial modulus",
+ NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
+ ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
}
- Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
- ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
+ return ret;
+ break;
}
- return ret;
- break;
- }
- case kind::ABS: {
- return nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
- break;
- }
+ case kind::ABS:
+ {
+ return nm->mkNode(kind::ITE,
+ nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))),
+ nm->mkNode(kind::UMINUS, node[0]),
+ node[0]);
+ break;
+ }
+ case kind::SQRT:
+ case kind::ARCSINE:
+ case kind::ARCCOSINE:
+ case kind::ARCTANGENT:
+ case kind::ARCCOSECANT:
+ case kind::ARCSECANT:
+ case kind::ARCCOTANGENT:
+ {
+ // eliminate inverse functions here
+ NodeMap::const_iterator it = d_nlin_inverse_skolem.find(node);
+ if (it == d_nlin_inverse_skolem.end())
+ {
+ Node var = nm->mkSkolem("nonlinearInv",
+ nm->realType(),
+ "the result of a non-linear inverse function");
+ d_nlin_inverse_skolem[node] = var;
+ Node lem;
+ if (k == kind::SQRT)
+ {
+ lem = nm->mkNode(kind::MULT, node[0], node[0]).eqNode(var);
+ }
+ else
+ {
+ Node pi = mkPi();
+
+ // range of the skolem
+ Node rlem;
+ if (k == kind::ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
+ {
+ Node half = nm->mkConst(Rational(1) / Rational(2));
+ Node pi2 = nm->mkNode(kind::MULT, half, pi);
+ Node npi2 = nm->mkNode(kind::MULT, nm->mkConst(Rational(-1)), pi2);
+ // -pi/2 < var <= pi/2
+ rlem = nm->mkNode(
+ AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
+ }
+ else
+ {
+ // 0 <= var < pi
+ rlem = nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
+ nm->mkNode(LT, var, pi));
+ }
+ if (options::nlExt())
+ {
+ d_nonlinearExtension->addDefinition(rlem);
+ }
- default:
- return node;
- break;
+ Kind rk = k == kind::ARCSINE
+ ? kind::SINE
+ : (k == kind::ARCCOSINE
+ ? kind::COSINE
+ : (k == kind::ARCTANGENT
+ ? kind::TANGENT
+ : (k == kind::ARCCOSECANT
+ ? kind::COSECANT
+ : (k == kind::ARCSECANT
+ ? kind::SECANT
+ : kind::COTANGENT))));
+ Node invTerm = nm->mkNode(rk, var);
+ // since invTerm may introduce division,
+ // we must also call expandDefinition on the result
+ invTerm = expandDefinition(logicRequest, invTerm);
+ lem = invTerm.eqNode(node[0]);
+ }
+ Assert(!lem.isNull());
+ if (options::nlExt())
+ {
+ d_nonlinearExtension->addDefinition(lem);
+ }
+ else
+ {
+ d_nlIncomplete = true;
+ }
+ return var;
+ }
+ return (*it).second;
+ break;
+ }
+
+ default: return node; break;
}
Unreachable();
* semantics. Needed to deal with partial function "mod".
*/
Node d_modZero;
-
- /**
- * Maps for Skolems for to-integer, real/integer div-by-k.
- * Introduced during ppRewriteTerms.
+
+ /**
+ * Maps for Skolems for to-integer, real/integer div-by-k, and inverse
+ * non-linear operators that are introduced during ppRewriteTerms.
*/
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
NodeMap d_to_int_skolem;
NodeMap d_div_skolem;
NodeMap d_int_div_skolem;
-
+ NodeMap d_nlin_inverse_skolem;
+
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
nta/exp-n0.5-lb.smt2 \
nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \
nta/NAVIGATION2.smt2 \
- nta/sin1-sat.smt2
+ nta/sin1-sat.smt2 \
+ nta/sugar-ident.smt2 \
+ nta/sugar-ident-2.smt2 \
+ nta/sugar-ident-3.smt2
# unsolved : garbage_collect.cvc
--- /dev/null
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+(declare-fun x3 () Real)
+(declare-fun x4 () Real)
+(declare-fun x5 () Real)
+
+(declare-fun a1 () Bool)
+(declare-fun a2 () Bool)
+(declare-fun a3 () Bool)
+(declare-fun a4 () Bool)
+(declare-fun a5 () Bool)
+(declare-fun a6 () Bool)
+(declare-fun a7 () Bool)
+
+(assert (= a2 (and (> (sin 1.0) 0.0) (> (cot 1.0) (/ (cos 1.0) (sin 1.0))))))
+(assert (= a7 (> (* (sec 1.0) (cos 1.0)) 1.0)))
+
+(assert (or
+a2
+a7
+))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun a6 () Bool)
+(assert (= a6 (> (* (csc 1.0) (sin 1.0)) 1.0)))
+(assert a6)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --nl-ext-tf-tplanes
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+(declare-fun x3 () Real)
+(declare-fun x4 () Real)
+(declare-fun x5 () Real)
+
+(declare-fun a1 () Bool)
+(declare-fun a3 () Bool)
+(declare-fun a4 () Bool)
+(declare-fun a5 () Bool)
+(declare-fun a6 () Bool)
+
+(assert (= a1 (not (= (sin (arcsin x1)) x1))))
+(assert (= a3 (< (arccos x3) 0)))
+(assert (= a4 (> (arctan x4) 1.8)))
+
+(assert (or a1 a3 a4))
+
+(check-sat)
projects / cvc5.git / commitdiff