Home
last modified time | relevance | path

Searched refs:LogicFormula (Results 1 – 18 of 18) sorted by relevance

/dports/lang/maude/maude-2.7.1/src/Higher/
H A DtemporalSymbol.cc119 TemporalSymbol::build(LogicFormula& formula, DagNodeSet& propositions, DagNode* dagNode) const in build()
123 return formula.makeOp(LogicFormula::LTL_TRUE); in build()
125 return formula.makeOp(LogicFormula::LTL_FALSE); in build()
128 LogicFormula::Op op = (s == notSymbol) ? LogicFormula::NOT : LogicFormula::NEXT; in build()
134 (op != LogicFormula::NOT || formula.getOp(a) == LogicFormula::PROPOSITION)) in build()
141 LogicFormula::Op op = (s == andSymbol) ? LogicFormula::AND : LogicFormula::OR; in build()
166 LogicFormula::Op op = (s == untilSymbol) ? LogicFormula::UNTIL : LogicFormula::RELEASE; in build()
H A DtemporalSymbol.hh45 int build(LogicFormula& formula, DagNodeSet& propositions, DagNode* dagNode) const;
H A DsatSolverSymbol.cc160 LogicFormula formula; in eqRewrite()
H A DmodelCheckerSymbol.cc254 LogicFormula formula; in eqRewrite()
H A DChangeLog2292 (build): check that formula under LogicFormula::NOT is a proposition
2347 * modelSymbol.hh: cleaned up includes; delete class LogicFormula
2476 inserting them into LogicFormula
2528 * logicFormula.hh (class LogicFormula): added decls for
2603 * higher.hh: added forward decls for classes LogicFormula,
/dports/lang/maude/maude-2.7.1/src/Temporal/
H A DveryWeakAlternatingAutomaton.cc65 case LogicFormula::AND: in dnf()
74 case LogicFormula::OR: in dnf()
102 case LogicFormula::PROPOSITION: in computeTransitionSet()
109 case LogicFormula::LTL_TRUE: in computeTransitionSet()
116 case LogicFormula::LTL_FALSE: in computeTransitionSet()
118 case LogicFormula::NOT: in computeTransitionSet()
125 case LogicFormula::NEXT: in computeTransitionSet()
140 case LogicFormula::AND: in computeTransitionSet()
145 case LogicFormula::OR: in computeTransitionSet()
156 if (op == LogicFormula::UNTIL) in computeTransitionSet()
[all …]
H A DlogicFormula.hh29 class LogicFormula class
80 inline LogicFormula::Op
81 LogicFormula::getOp(int nodeNr) const in getOp()
87 LogicFormula::getProp(int nodeNr) const in getProp()
93 LogicFormula::getArg(int nodeNr, int argNr) const in getArg()
99 LogicFormula::isPropositional(int nodeNr) const in isPropositional()
H A DlogicFormula.cc36 LogicFormula::makeProp(int propIndex) in makeProp()
54 LogicFormula::makeOp(Op op, int firstArg, int secondArg) in makeOp()
222 LogicFormula::dump(ostream& s) in dump()
H A DveryWeakAlternatingAutomaton.hh41 VeryWeakAlternatingAutomaton(LogicFormula* formula, int top);
64 LogicFormula* const formula;
H A Dtemporal.hh29 class LogicFormula;
H A DChangeLog8 * logicFormula.hh (class LogicFormula): TRUE -> LTL_TRUE,
109 * logicFormula.hh (class LogicFormula): added propositional field
210 (computeTransitionSet): turned op == LogicFormula::RELEASE into an
282 * modelChecker2.hh: removed class LogicFormula hack
300 * veryWeakAlternatingAutomaton.hh: removed class LogicFormula hack
H A DmodelChecker2.hh48 ModelChecker2(System& system, LogicFormula& property, int top);
H A DbuchiAutomaton2.hh39 BuchiAutomaton2(LogicFormula* formula, int top);
H A DgenBuchiAutomaton.hh55 GenBuchiAutomaton(LogicFormula* formula, int top);
H A DmodelChecker2.cc37 ModelChecker2::ModelChecker2(System& system, LogicFormula& property, int top) in ModelChecker2()
H A DbuchiAutomaton2.cc38 BuchiAutomaton2::BuchiAutomaton2(LogicFormula* formula, int top) in BuchiAutomaton2()
H A DgenBuchiAutomaton.cc44 GenBuchiAutomaton::GenBuchiAutomaton(LogicFormula* formula, int top) in GenBuchiAutomaton()
/dports/lang/maude/maude-2.7.1/src/Utility/
H A DChangeLog2262 (class LogicFormula): store propositions as ints rather than