1 /********************* */
2 /*! \file theory_arith.cpp
4 ** Top contributors (to current version):
5 ** Tim King, Andrew Reynolds, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/arith/theory_arith.h"
20 #include "options/smt_options.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "theory/arith/arith_rewriter.h"
23 #include "theory/arith/infer_bounds.h"
24 #include "theory/arith/theory_arith_private.h"
25 #include "theory/ext_theory.h"
28 using namespace CVC4::kind
;
34 TheoryArith::TheoryArith(context::Context
* c
, context::UserContext
* u
,
35 OutputChannel
& out
, Valuation valuation
,
36 const LogicInfo
& logicInfo
)
37 : Theory(THEORY_ARITH
, c
, u
, out
, valuation
, logicInfo
)
38 , d_internal(new TheoryArithPrivate(*this, c
, u
, out
, valuation
, logicInfo
))
39 , d_ppRewriteTimer("theory::arith::ppRewriteTimer")
40 , d_proofRecorder(nullptr)
42 smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer
);
43 if (options::nlExt()) {
45 getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT
);
46 getExtTheory()->addFunctionKind(kind::EXPONENTIAL
);
47 getExtTheory()->addFunctionKind(kind::SINE
);
48 getExtTheory()->addFunctionKind(kind::PI
);
52 TheoryArith::~TheoryArith(){
53 smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer
);
57 TheoryRewriter
* TheoryArith::getTheoryRewriter()
59 return d_internal
->getTheoryRewriter();
62 void TheoryArith::preRegisterTerm(TNode n
){
63 d_internal
->preRegisterTerm(n
);
66 void TheoryArith::finishInit()
68 TheoryModel
* tm
= d_valuation
.getModel();
69 Assert(tm
!= nullptr);
70 if (getLogicInfo().isTheoryEnabled(THEORY_ARITH
)
71 && getLogicInfo().areTranscendentalsUsed())
73 // witness is used to eliminate square root
74 tm
->setUnevaluatedKind(kind::WITNESS
);
75 // we only need to add the operators that are not syntax sugar
76 tm
->setUnevaluatedKind(kind::EXPONENTIAL
);
77 tm
->setUnevaluatedKind(kind::SINE
);
78 tm
->setUnevaluatedKind(kind::PI
);
82 Node
TheoryArith::expandDefinition(Node node
)
84 return d_internal
->expandDefinition(node
);
87 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
88 d_internal
->setMasterEqualityEngine(eq
);
91 void TheoryArith::addSharedTerm(TNode n
){
92 d_internal
->addSharedTerm(n
);
95 Node
TheoryArith::ppRewrite(TNode atom
) {
96 CodeTimer
timer(d_ppRewriteTimer
, /* allow_reentrant = */ true);
97 return d_internal
->ppRewrite(atom
);
100 Theory::PPAssertStatus
TheoryArith::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
101 return d_internal
->ppAssert(in
, outSubstitutions
);
104 void TheoryArith::ppStaticLearn(TNode n
, NodeBuilder
<>& learned
) {
105 d_internal
->ppStaticLearn(n
, learned
);
108 void TheoryArith::check(Effort effortLevel
){
109 getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep
);
110 d_internal
->check(effortLevel
);
113 bool TheoryArith::needsCheckLastEffort() {
114 return d_internal
->needsCheckLastEffort();
117 Node
TheoryArith::explain(TNode n
) {
118 return d_internal
->explain(n
);
121 bool TheoryArith::getCurrentSubstitution( int effort
, std::vector
< Node
>& vars
, std::vector
< Node
>& subs
, std::map
< Node
, std::vector
< Node
> >& exp
) {
122 return d_internal
->getCurrentSubstitution( effort
, vars
, subs
, exp
);
125 bool TheoryArith::isExtfReduced( int effort
, Node n
, Node on
, std::vector
< Node
>& exp
) {
126 return d_internal
->isExtfReduced( effort
, n
, on
, exp
);
129 void TheoryArith::propagate(Effort e
) {
130 d_internal
->propagate(e
);
132 bool TheoryArith::collectModelInfo(TheoryModel
* m
)
134 return d_internal
->collectModelInfo(m
);
137 void TheoryArith::notifyRestart(){
138 d_internal
->notifyRestart();
141 void TheoryArith::presolve(){
142 d_internal
->presolve();
145 EqualityStatus
TheoryArith::getEqualityStatus(TNode a
, TNode b
) {
146 return d_internal
->getEqualityStatus(a
,b
);
149 Node
TheoryArith::getModelValue(TNode var
) {
150 return d_internal
->getModelValue( var
);
154 std::pair
<bool, Node
> TheoryArith::entailmentCheck (TNode lit
,
155 const EntailmentCheckParameters
* params
,
156 EntailmentCheckSideEffects
* out
)
158 const ArithEntailmentCheckParameters
* aparams
= NULL
;
160 ArithEntailmentCheckParameters
* def
= new ArithEntailmentCheckParameters();
161 def
->addLookupRowSumAlgorithms();
164 AlwaysAssert(params
->getTheoryId() == getId());
165 aparams
= dynamic_cast<const ArithEntailmentCheckParameters
*>(params
);
167 Assert(aparams
!= NULL
);
169 ArithEntailmentCheckSideEffects
* ase
= NULL
;
171 ase
= new ArithEntailmentCheckSideEffects();
173 AlwaysAssert(out
->getTheoryId() == getId());
174 ase
= dynamic_cast<ArithEntailmentCheckSideEffects
*>(out
);
178 std::pair
<bool, Node
> res
= d_internal
->entailmentCheck(lit
, *aparams
, *ase
);
190 }/* CVC4::theory::arith namespace */
191 }/* CVC4::theory namespace */
192 }/* CVC4 namespace */