API tools faq
paste
Advertisement
Guest User

8

a guest
Sep 20th, 2017
83
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
C++ 40.31 KB | None | 0 0
raw download clone embed print report
  1. #include <iostream>
  2. #include <set>
  3. #include <map>
  4. #include <string>
  5. #include <sstream>
  6. #include <vector>
  7. #include <algorithm>
  8. #include <memory>
  9. #include <functional>
  10.  
  11. using namespace std;
  12.  
  13. /* Funkcijski i predikatski simboli */
  14. typedef string FunctionSymbol;
  15. typedef string PredicateSymbol;
  16.  
  17. /* Signatura se sastoji iz funkcijskih i predikatskih simbola kojima
  18.    su pridruzene arnosti (nenegativni celi brojevi) */
  19. class Signature {
  20. private:
  21.   map<FunctionSymbol,  unsigned> _functions;
  22.   map<PredicateSymbol, unsigned> _predicates;
  23. public:
  24.  
  25.   /* Dodavanje funkcijskog simbola date arnosti */
  26.   void addFunctionSymbol(const FunctionSymbol & f, unsigned arity);
  27.  
  28.   /* Dodavanje predikatskog simbola date arnosti */
  29.   void addPredicateSymbol(const PredicateSymbol & p, unsigned arity);
  30.  
  31.   /* Provera da li postoji dati funkcijski simbol, i koja mu je arnost */
  32.   bool checkFunctionSymbol(const FunctionSymbol & f, unsigned & arity) const;
  33.  
  34.   /* Provera da li postoji dati predikatski simbol, i koja mu je arnost */
  35.   bool checkPredicateSymbol(const PredicateSymbol & f, unsigned & arity) const;
  36.  
  37. };
  38.  
  39.  
  40. /* Tip podatka za predstavljanje varijable */
  41. typedef string Variable;
  42.  
  43. /* Skup varijabli */
  44. typedef set<Variable> VariableSet;
  45.  
  46.  
  47. class Structure; // L-strukture (videti dole)
  48. class Valuation; // Valuacija (videti dole)
  49.  
  50. class BaseTerm;
  51. typedef std::shared_ptr<BaseTerm> Term;
  52.  
  53. /* Apstraktna klasa BaseTerm koja predstavlja termove */
  54. class BaseTerm : public enable_shared_from_this<BaseTerm> {
  55.  
  56. public:
  57.   /* Termovi mogu biti ili varijable ili funkcijski simboli primenjeni
  58.      na (0 ili vise) termova */
  59.   enum Type { TT_VARIABLE, TT_FUNCTION };
  60.  
  61.   /* Vraca tip terma */
  62.   virtual Type getType() const = 0;
  63.  
  64.   /* Prikazuje term */
  65.   virtual void printTerm(ostream & ostr) const = 0;
  66.  
  67.   /* Ispituje sintaksnu jednakost termova */
  68.   virtual bool equalTo(const Term & t) const = 0;
  69.  
  70.   /* Vraca skup svih varijabli koje se pojavljuju u termu */
  71.   virtual void getVars(VariableSet & vars) const = 0;
  72.  
  73.   /* Odredjuje da li se data varijabla nalazi u termu */
  74.   bool containsVariable(const Variable & v) const;
  75.  
  76.   /* Odredjuje interpretaciju terma u datoj L-strukturi i datoj valuaciji */
  77.   virtual unsigned eval(const Structure & st, const Valuation & val) const = 0;
  78.  
  79.   /* Zamena varijable v termom t */
  80.   virtual Term substitute(const Variable & v, const Term & t) = 0;
  81.  
  82.   virtual ~BaseTerm() {}
  83. };
  84.  
  85. ostream & operator << (ostream & ostr, const Term & t);
  86.  
  87. /* Term koji predstavlja jednu varijablu */
  88. class VariableTerm : public BaseTerm {
  89. private:
  90.   Variable _v;
  91. public:
  92.   VariableTerm(const Variable & v);
  93.   virtual Type getType() const;
  94.   const Variable & getVariable() const;
  95.   virtual void printTerm(ostream & ostr) const;
  96.   virtual bool equalTo(const Term & t) const;
  97.   virtual void getVars(VariableSet & vars) const;
  98.   virtual unsigned eval(const Structure & st, const Valuation & val) const;
  99.   virtual Term substitute(const Variable & v, const Term & t);
  100. };
  101.  
  102. /* Term koji predstavlja funkcijski simbol primenjen na odgovarajuci
  103.    broj podtermova */
  104. class FunctionTerm : public BaseTerm {
  105. private:
  106.   const Signature & _sig;
  107.   FunctionSymbol _f;
  108.   vector<Term> _ops;
  109.  
  110. public:
  111.   FunctionTerm(const Signature & s, const FunctionSymbol & f,
  112.            const vector<Term> & ops);
  113.   FunctionTerm(const Signature & s, const FunctionSymbol & f,
  114.            vector<Term> && ops = vector<Term> ());
  115.   virtual Type getType() const;
  116.   const Signature & getSignature() const;
  117.   const FunctionSymbol & getSymbol() const;
  118.   const vector<Term> & getOperands() const;
  119.   virtual void printTerm(ostream & ostr) const;
  120.   virtual bool equalTo(const Term & t) const;
  121.   virtual void getVars(VariableSet & vars) const;
  122.   virtual unsigned eval(const Structure & st, const Valuation & val) const;
  123.   virtual Term substitute(const Variable & v, const Term & t);
  124. };
  125.  
  126.  
  127. class BaseFormula;
  128. typedef std::shared_ptr<BaseFormula> Formula;
  129.  
  130. /* Apstraktna klasa kojom se predstavljaju formule */
  131. class BaseFormula : public enable_shared_from_this<BaseFormula> {
  132.  
  133. public:
  134.  
  135.   /* Tipovi formula (dodatak u odnosu na iskaznu logiku su formule
  136.      kod kojih je vodeci simbol univerzalni ili egzistencijalni
  137.      kvantifikator */
  138.   enum Type { T_TRUE, T_FALSE, T_ATOM, T_NOT,
  139.           T_AND, T_OR, T_IMP, T_IFF, T_FORALL, T_EXISTS };
  140.  
  141.   /* Prikaz formule */
  142.   virtual void printFormula(ostream & ostr) const = 0;
  143.  
  144.   /* Tip formule */
  145.   virtual Type getType() const = 0;
  146.  
  147.   /* Slozenost formule */
  148.   virtual unsigned complexity() const = 0;
  149.  
  150.   /* Sintaksna jednakost dve formule */
  151.   virtual bool equalTo(const Formula & f) const = 0;
  152.  
  153.   /* Ocitava sve varijable koje se pojavljuju u formuli. Ako
  154.      je zadat drugi parametar sa vrednoscu true, tada se izdvajaju samo
  155.      slobodne varijable u formuli */
  156.   virtual void getVars(VariableSet & vars, bool free = false) const = 0;
  157.  
  158.   /* Ispituje da li se varijabla pojavljuje u formuli (kao slobodna ili
  159.      vezana) */
  160.   bool containsVariable(const Variable & v, bool free = false) const;
  161.  
  162.   /* Izracunava interpretaciju formule za datu L-strukturu i valuaciju */
  163.   virtual bool eval(const Structure & st, const Valuation & val) const = 0;
  164.  
  165.   /* Zamena slobodnih pojavljivanja varijable v termom t */
  166.   virtual Formula substitute(const Variable & v, const Term & t) = 0;
  167.  
  168.   virtual ~BaseFormula() {}
  169. };
  170.  
  171. ostream & operator << (ostream & ostr, const Formula & f);
  172.  
  173. /* Funkcija vraca novu varijablu koja se ne pojavljuje ni u f ni u t */
  174. Variable getUniqueVariable(const Formula & f, const Term & t);
  175.  
  176. /* Klasa predstavlja sve atomicke formule (True, False i Atom) */
  177. class AtomicFormula : public BaseFormula {
  178.  
  179. public:
  180.   virtual unsigned complexity() const;
  181. };
  182.  
  183. /* Klasa predstavlja logicke konstante (True i False) */
  184. class LogicConstant : public AtomicFormula {
  185.  
  186. public:
  187.   virtual bool equalTo(const Formula & f) const;
  188.   virtual void getVars(VariableSet & vars, bool free) const;
  189.   virtual Formula substitute(const Variable & v, const Term & t);
  190. };
  191.  
  192. /* Klasa predstavlja True logicku konstantu */
  193. class True : public LogicConstant {
  194.  
  195. public:
  196.   virtual void printFormula(ostream & ostr) const;
  197.   virtual Type getType() const;
  198.   virtual bool eval(const Structure & st,
  199.             const Valuation & val) const;
  200. };
  201.  
  202. /* Klasa predstavlja logicku konstantu False */
  203. class False : public LogicConstant {
  204.  
  205. public:
  206.   virtual void printFormula(ostream & ostr) const;
  207.   virtual Type getType() const;
  208.   virtual bool eval(const Structure & st,
  209.             const Valuation & val) const;
  210. };
  211.  
  212. /* Klasa predstavlja atom, koji za razliku od iskazne logike ovde ima
  213.    znatno slozeniju strukturu. Svaki atom je predikatski simbol primenjen
  214.    na odgovarajuci broj podtermova */
  215. class Atom : public AtomicFormula {
  216. private:
  217.   const Signature & _sig;
  218.   PredicateSymbol _p;
  219.   vector<Term> _ops;
  220.  
  221. public:
  222.   Atom(const Signature & s,
  223.        const PredicateSymbol & p,
  224.        const vector<Term> & ops);
  225.   Atom(const Signature & s,
  226.        const PredicateSymbol & p,
  227.        vector<Term> && ops = vector<Term>());
  228.   const PredicateSymbol & getSymbol() const;
  229.   const Signature & getSignature() const;
  230.   const vector<Term> & getOperands() const;
  231.   virtual void printFormula(ostream & ostr) const;
  232.   virtual Type getType() const;
  233.   virtual bool equalTo(const Formula & f) const;
  234.  
  235.   virtual void getVars(VariableSet & vars, bool free) const;
  236.   virtual bool eval(const Structure & st,
  237.             const Valuation & val) const;
  238.   virtual Formula substitute(const Variable & v, const Term & t);
  239. };
  240.  
  241.  
  242. /* Klasa unarni veznik (obuhvata negaciju) */
  243. class UnaryConnective : public BaseFormula {
  244. protected:
  245.   Formula _op;
  246. public:
  247.   UnaryConnective(const Formula & op);
  248.   const Formula & getOperand() const;
  249.   virtual unsigned complexity() const;
  250.   virtual bool equalTo(const Formula & f) const;
  251.   virtual void getVars(VariableSet & vars, bool free) const;
  252. };
  253.  
  254. /* Klasa koja predstavlja negaciju */
  255. class Not : public UnaryConnective {
  256. public:
  257.  
  258.   using UnaryConnective::UnaryConnective;
  259.   virtual void printFormula(ostream & ostr) const;
  260.   virtual Type getType() const;
  261.   virtual bool eval(const Structure & st,
  262.             const Valuation & val) const;
  263.   virtual Formula substitute(const Variable & v, const Term & t);
  264. };
  265.  
  266. /* Klasa predstavlja sve binarne veznike */
  267. class BinaryConnective : public BaseFormula {
  268. protected:
  269.    Formula _op1, _op2;
  270. public:
  271.   BinaryConnective(const Formula & op1, const Formula & op2);
  272.   const Formula & getOperand1() const;
  273.   const Formula & getOperand2() const;
  274.   virtual unsigned complexity() const;
  275.   virtual bool equalTo(const Formula & f) const;
  276.   virtual void getVars(VariableSet & vars, bool free) const;
  277. };
  278.  
  279. /* Klasa predstavlja konjunkciju */
  280. class And : public BinaryConnective {
  281. public:
  282.   using BinaryConnective::BinaryConnective;
  283.   virtual void printFormula(ostream & ostr) const;
  284.   virtual Type getType() const;
  285.   virtual bool eval(const Structure & st,
  286.             const Valuation & val) const;
  287.   virtual Formula substitute(const Variable & v, const Term & t);
  288.  };
  289.  
  290.  
  291. /* Klasa predstavlja disjunkciju */
  292. class Or : public BinaryConnective {
  293. public:
  294.   using BinaryConnective::BinaryConnective;
  295.   virtual void printFormula(ostream & ostr) const;
  296.   virtual Type getType() const;
  297.   virtual bool eval(const Structure & st,
  298.             const Valuation & val) const;
  299.   virtual Formula substitute(const Variable & v, const Term & t);
  300. };
  301.  
  302. /* Klasa predstavlja implikaciju */
  303. class Imp : public BinaryConnective {
  304. public:
  305.   using BinaryConnective::BinaryConnective;
  306.   virtual void printFormula(ostream & ostr) const;
  307.   virtual Type getType() const;
  308.   virtual bool eval(const Structure & st,
  309.             const Valuation & val) const;
  310.   virtual Formula substitute(const Variable & v, const Term & t);
  311. };
  312.  
  313.  
  314. /* Klasa predstavlja ekvivalenciju */
  315. class Iff : public BinaryConnective {
  316.  
  317. public:
  318.   using BinaryConnective::BinaryConnective;
  319.   virtual void printFormula(ostream & ostr) const;
  320.   virtual Type getType() const;
  321.   virtual bool eval(const Structure & st,
  322.             const Valuation & val) const;
  323.   virtual Formula substitute(const Variable & v, const Term & t);
  324. };
  325.  
  326. /* Klasa predstavlja kvantifikovane formule */
  327. class Quantifier : public BaseFormula {
  328. protected:
  329.   Variable _v;
  330.   Formula _op;
  331.  
  332. public:
  333.   Quantifier(const Variable & v, const Formula & op);
  334.   const Variable & getVariable() const;
  335.   const Formula & getOperand() const;
  336.   virtual unsigned complexity() const;
  337.   virtual bool equalTo(const Formula & f) const;
  338.   virtual void getVars(VariableSet & vars, bool free) const;
  339. };
  340.  
  341.  
  342. /* Klasa predstavlja univerzalno kvantifikovanu formulu */
  343. class Forall : public Quantifier {
  344. public:
  345.   using Quantifier::Quantifier;
  346.   virtual Type getType() const;
  347.   virtual void printFormula(ostream & ostr) const;
  348.   virtual bool eval(const Structure & st,
  349.             const Valuation & val) const;
  350.   virtual Formula substitute(const Variable & v, const Term & t);
  351. };
  352.  
  353.  
  354. /* Klasa predstavlja egzistencijalnog kvantifikatora */
  355. class Exists : public Quantifier {
  356. public:
  357.   using Quantifier::Quantifier;
  358.   virtual Type getType() const;
  359.   virtual void printFormula(ostream & ostr) const;
  360.   virtual bool eval(const Structure & st,
  361.             const Valuation & val) const;
  362.   virtual Formula substitute(const Variable & v, const Term & t);
  363. };
  364.  
  365.  
  366.  
  367. /* Tip podataka kojim se predstavlja domen. U opstem slucaju, domen u logici
  368.    prvog reda moze biti i beskonacan skup. Medjutim, mi cemo se u nasoj
  369.    implementaciji zadrzati na konacnim skupovima, kako bismo mogli da
  370.    simuliramo izracunavanje interpretacija kvantifikovanih formula. Zato
  371.    ce nam domen uvek biti neki konacan podskup skupa prirodnih brojeva */
  372. typedef std::vector<unsigned> Domain;
  373.  
  374. /* Apstraktni tip podatka kojim se predstavlja funkcija D^n --> D kojom
  375.    se mogu interpretirati funkcijski simboli arnosti n */
  376. class Function {
  377. private:
  378.   unsigned _arity;
  379. public:
  380.   Function(unsigned arity);
  381.   unsigned getArity();
  382.   virtual unsigned eval(const vector<unsigned> & args = vector<unsigned>()) = 0;
  383.   virtual ~Function() {}
  384. };
  385.  
  386.  
  387. /* Apstraktni tip podataka kojim se predstavlja relacija D^n --> {0,1} kojom
  388.    se mogu interpretirati predikatski simboli arnosti n */
  389. class Relation {
  390. private:
  391.   unsigned _arity;
  392. public:
  393.   Relation(unsigned arity);
  394.   unsigned getArity();
  395.   virtual bool eval(const vector<unsigned> & args = vector<unsigned>()) = 0;
  396.   virtual ~Relation() {}
  397. };
  398.  
  399. /* Klasa koja predstavlja L-strukturu (ili model) nad signaturom L i domenom
  400.    D. Model svakom funkcijskom simbolu pridruzuje funkciju odgovarajuce
  401.    arnosti, dok svakom predikatskom simbolu pridruzuje relaciju odgovarajuce
  402.    arnosti. */
  403. class Structure {
  404. private:
  405.   const Signature & _sig;
  406.   const Domain & _domain;
  407.   map<FunctionSymbol, Function *> _funs;
  408.   map<PredicateSymbol, Relation *> _rels;
  409.  
  410. public:
  411.   Structure(const Signature & sig, const Domain & domain);
  412.  
  413.   const Signature & getSignature() const;
  414.   const Domain & getDomain() const;
  415.  
  416.   /* Dodavanje interpretacije funkcijskom simbolu */
  417.   void addFunction(const FunctionSymbol & fs, Function * f);
  418.  
  419.   /* Citanje interpretacije datog funkcijskog simbola */
  420.   Function * getFunction(const FunctionSymbol & f) const;
  421.  
  422.   /* Dodavanje interpretacije predikatskom simbolu */
  423.   void addRelation(const PredicateSymbol & ps, Relation * r);
  424.  
  425.   /* Citanje interpretacije datog predikatskog simbola */
  426.   Relation * getRelation(const PredicateSymbol & p) const;
  427.  
  428.   ~Structure();
  429. };
  430.  
  431. /* Klasa kojom se predstavlja valuacija. Valuacijom (nad datim domenom) se
  432.    svakoj varijabli dodeljuje neka vrednost iz domena. Drugim recima,
  433.    valuacija odredjuje interpretaciju varijabli. */
  434. class Valuation {
  435. private:
  436.   const Domain & _domain;
  437.   map<Variable, unsigned> _values;
  438. public:
  439.   Valuation(const Domain & dom);
  440.   const Domain & getDomain() const;
  441.  
  442.   /* Postavljanje vrednosti date varijable na datu vrednost */
  443.   void setValue(const Variable & v, unsigned value);
  444.  
  445.   /* Ocitavanje vrednosti date varijable */
  446.   unsigned getValue(const Variable & v) const;
  447. };
  448.  
  449.  
  450. // Definicije funkcija clanica -----------------------------------------
  451.  
  452. // Funkcije substitucije -----------------------------------------------
  453.  
  454. Term VariableTerm::substitute(const Variable & v, const Term & t)
  455. {
  456.   if(_v == v)
  457.     return t;
  458.   else
  459.     return shared_from_this();
  460. }
  461.  
  462. Term FunctionTerm::substitute(const Variable & v, const Term & t)
  463. {
  464.   vector<Term> sub_ops;
  465.  
  466.   for(unsigned i = 0; i < _ops.size(); i++)
  467.     sub_ops.push_back(_ops[i]->substitute(v, t));
  468.  
  469.   return make_shared<FunctionTerm>(_sig, _f, sub_ops);
  470. }
  471.  
  472. Formula LogicConstant::substitute(const Variable & v, const Term & t)
  473. {
  474.   return shared_from_this();
  475. }
  476.  
  477. Formula Atom::substitute(const Variable & v, const Term & t)
  478. {
  479.   vector<Term> sub_ops;
  480.    
  481.   for(unsigned i = 0; i < _ops.size(); i++)
  482.     sub_ops.push_back(_ops[i]->substitute(v, t));
  483.  
  484.   return make_shared<Atom>(_sig, _p, sub_ops);
  485. }
  486.  
  487. Formula Not::substitute(const Variable & v, const Term & t)
  488. {
  489.   return make_shared<Not>(_op->substitute(v, t));
  490. }
  491.  
  492. Formula And::substitute(const Variable & v, const Term & t)
  493. {
  494.   return make_shared<And>(_op1->substitute(v, t), _op2->substitute(v, t));
  495. }
  496.  
  497. Formula Or::substitute(const Variable & v, const Term & t)
  498. {
  499.   return make_shared<Or>(_op1->substitute(v, t), _op2->substitute(v, t));
  500. }
  501.  
  502. Formula Imp::substitute(const Variable & v, const Term & t)
  503. {
  504.   return make_shared<Imp>(_op1->substitute(v, t), _op2->substitute(v, t));
  505. }
  506.  
  507. Formula Iff::substitute(const Variable & v, const Term & t)
  508. {
  509.   return make_shared<Iff>(_op1->substitute(v, t), _op2->substitute(v, t));
  510. }
  511.  
  512.  
  513. Formula Forall::substitute(const Variable & v, const Term & t)
  514. {
  515.   if(v == _v)
  516.     return shared_from_this();
  517.    
  518.   /* Ako term sadrzi kvantifikovanu varijablu, tada moramo najpre
  519.      preimenovati kvantifikovanu varijablu (nekom varijablom koja
  520.      nije sadzana ni u termu ni u formuli sto nam daje funkcija
  521.      getUniqueVariable koja je clanica klase Quantifier) */
  522.     if(t->containsVariable(_v))
  523.       {
  524.     Variable new_v = getUniqueVariable(shared_from_this(), t);
  525.     Formula sub_op = _op->substitute(_v, make_shared<VariableTerm>(new_v));
  526.     return make_shared<Forall>(new_v, sub_op->substitute(v, t));
  527.       }
  528.     else
  529.       return make_shared<Forall>(_v, _op->substitute(v, t));
  530. }
  531.  
  532. Formula Exists::substitute(const Variable & v, const Term & t)
  533. {
  534.   if(v == _v)
  535.     return shared_from_this();
  536.  
  537.   /* Ako term sadrzi kvantifikovanu varijablu, tada moramo najpre
  538.      preimenovati kvantifikovanu varijablu (nekom varijablom koja
  539.      nije sadzana ni u termu ni u formuli sto nam daje funkcija
  540.      getUniqueVariable koja je clanica klase Quantifier) */
  541.   if(t->containsVariable(_v))
  542.     {
  543.       Variable new_v = getUniqueVariable(shared_from_this(), t);
  544.      
  545.       Formula sub_op = _op->substitute(_v, make_shared<VariableTerm>(new_v));
  546.       return make_shared<Exists>(new_v, sub_op->substitute(v, t));
  547.     }
  548.   else
  549.     return make_shared<Exists>(_v, _op->substitute(v, t));
  550. }
  551.  
  552. // ---------------------------------------------------------------------
  553.  
  554. // Funkcije za odredjivanje sintaksne identicnosti termova i formula ---
  555.  
  556. bool VariableTerm::equalTo(const Term & t) const
  557. {
  558.   return t->getType() == TT_VARIABLE &&
  559.     ((VariableTerm *) t.get())->getVariable() == _v;
  560. }
  561.  
  562. bool FunctionTerm::equalTo(const Term & t) const
  563. {
  564.   if(t->getType() != TT_FUNCTION)
  565.     return false;
  566.  
  567.   if(_f != ((FunctionTerm *) t.get())->getSymbol())
  568.     return false;
  569.  
  570.   const vector<Term> & t_ops = ((FunctionTerm *) t.get())->getOperands();
  571.  
  572.   if(_ops.size() != t_ops.size())
  573.     return false;
  574.  
  575.   for(unsigned i = 0; i < _ops.size(); i++)
  576.     if(!_ops[i]->equalTo(t_ops[i]))
  577.       return false;
  578.  
  579.   return true;
  580. }
  581.  
  582. bool LogicConstant::equalTo( const Formula & f) const
  583. {
  584.   return f->getType() == this->getType();
  585. }
  586.  
  587.  
  588. bool Atom::equalTo(const Formula & f) const
  589. {
  590.   if(f->getType() != T_ATOM)
  591.     return false;
  592.  
  593.   if(_p != ((Atom *) f.get())->getSymbol())
  594.     return false;
  595.  
  596.   const vector<Term> & f_ops = ((Atom *) f.get())->getOperands();
  597.  
  598.   if(_ops.size() != f_ops.size())
  599.     return false;
  600.  
  601.   for(unsigned i = 0; i < _ops.size(); i++)
  602.     if(!_ops[i]->equalTo(f_ops[i]))
  603.       return false;
  604.  
  605.     return true;
  606. }
  607.  
  608. bool UnaryConnective::equalTo(const Formula & f) const
  609. {
  610.   return f->getType() == this->getType() &&
  611.     _op->equalTo(((UnaryConnective *)f.get())->getOperand());
  612. }
  613.  
  614. bool BinaryConnective::equalTo( const Formula & f) const
  615. {
  616.   return f->getType() == this->getType() &&
  617.     _op1->equalTo(((BinaryConnective *)f.get())->getOperand1())
  618.     &&  
  619.     _op2->equalTo(((BinaryConnective *)f.get())->getOperand2());
  620. }
  621.  
  622. bool Quantifier::equalTo(const Formula & f) const
  623. {
  624.   return f->getType() == getType() &&
  625.     ((Quantifier *) f.get())->getVariable() == _v &&
  626.     ((Quantifier *) f.get())->getOperand()->equalTo(_op);
  627. }
  628.  
  629. // ---------------------------------------------------------------------
  630.  
  631. // Funkcije za odredjivanje skupa varijabli ----------------------------
  632.  
  633. void VariableTerm::getVars(VariableSet & vars) const
  634. {
  635.   vars.insert(_v);
  636. }
  637.  
  638. void FunctionTerm::getVars(VariableSet & vars) const
  639. {
  640.   for(unsigned i = 0; i < _ops.size(); i++)
  641.     _ops[i]->getVars(vars);
  642. }
  643.  
  644. void LogicConstant::getVars(VariableSet & vars, bool free) const
  645. {
  646.   return;
  647. }
  648.  
  649. void Atom::getVars(VariableSet & vars, bool free) const
  650. {
  651.   for(unsigned i = 0; i < _ops.size(); i++)
  652.     {
  653.       _ops[i]->getVars(vars);
  654.     }
  655. }
  656.  
  657. void UnaryConnective::getVars(VariableSet & vars, bool free) const
  658. {
  659.   _op->getVars(vars, free);
  660. }
  661.  
  662. void BinaryConnective::getVars(VariableSet & vars, bool free) const
  663. {
  664.   _op1->getVars(vars, free);
  665.   _op2->getVars(vars, free);
  666. }
  667.  
  668. void Quantifier::getVars(VariableSet & vars, bool free) const
  669. {
  670.   bool present = false;
  671.  
  672.   if(free)
  673.     {
  674.       /* Pamtimo da li je kvantifikovana varijabla vec u skupu slobodnih
  675.      varijabli */
  676.       if(vars.find(_v) != vars.end())
  677.     present = true;
  678.     }
  679.  
  680.   _op->getVars(vars, free);
  681.   if(!free)
  682.     vars.insert(_v);
  683.  
  684.   if(free)
  685.     {
  686.       /* Ako varijabla ranije nije bila prisutna u skupu slobodnih varijabli,
  687.      tada je brisemo, zato sto to znaci da se ona pojavljuje samo u
  688.      podformuli kvantifikovane formule,a u njoj je vezana kvantifikatorom */
  689.       if(!present && vars.find(_v) != vars.end())
  690.     vars.erase(_v);
  691.     }
  692. }
  693.  
  694. // ---------------------------------------------------------------------
  695.  
  696. // Funkcije za odredjivanje slozenosti formule -------------------------
  697.  
  698. unsigned AtomicFormula::complexity() const
  699. {
  700.   return 0;
  701. }  
  702.  
  703. unsigned UnaryConnective::complexity() const
  704. {
  705.   return _op->complexity() + 1;
  706. }
  707.  
  708. unsigned BinaryConnective::complexity() const
  709. {
  710.   return _op1->complexity() + _op2->complexity() + 1;
  711. }
  712.  
  713. unsigned Quantifier::complexity() const
  714. {
  715.   return _op->complexity() + 1;
  716. }
  717.  
  718. // ---------------------------------------------------------------------
  719.  
  720. // Funkcije za stampanje -----------------------------------------------
  721.  
  722.  
  723. void VariableTerm::printTerm(ostream & ostr) const
  724. {
  725.   ostr << _v;
  726. }
  727.  
  728. void FunctionTerm::printTerm(ostream & ostr) const
  729. {
  730.   ostr << _f;
  731.  
  732.   for(unsigned i = 0; i < _ops.size(); i++)
  733.     {
  734.       if(i == 0)
  735.     ostr << "(";
  736.       ostr << _ops[i];
  737.       if(i != _ops.size() - 1)
  738.     ostr << ",";
  739.       else
  740.     ostr << ")";
  741.     }
  742. }
  743.  
  744. void True::printFormula(ostream & ostr) const
  745. {
  746.   ostr << "True";
  747. }
  748.  
  749. void False::printFormula(ostream & ostr) const
  750. {
  751.   ostr << "False";
  752. }
  753.  
  754. void Atom::printFormula(ostream & ostr) const
  755. {
  756.   ostr << _p;
  757.   for(unsigned i = 0; i < _ops.size(); i++)
  758.     {
  759.       if(i == 0)
  760.     ostr << "(";
  761.       ostr << _ops[i];
  762.       if(i != _ops.size() - 1)
  763.     ostr << ",";
  764.       else
  765.     ostr << ")";
  766.     }
  767. }
  768.  
  769. void Not::printFormula(ostream & ostr) const
  770. {
  771.   ostr << "(~" << _op << ")";
  772. }
  773.  
  774. void And::printFormula(ostream & ostr) const
  775. {
  776.   ostr << "(" << _op1 << " /\\ " << _op2 << ")";
  777. }
  778.  
  779. void Or::printFormula(ostream & ostr) const
  780. {
  781.   ostr << "(" << _op1 << " \\/ " << _op2 << ")";
  782. }
  783.  
  784. void Imp::printFormula(ostream & ostr) const
  785. {
  786.   ostr << "(" << _op1 << " ==> " << _op2 << ")";
  787. }
  788.  
  789. void Iff::printFormula(ostream & ostr) const
  790. {
  791.   ostr << "(" << _op1 << " <=> " << _op2 << ")";
  792. }
  793.  
  794. void Forall::printFormula(ostream & ostr) const
  795. {
  796.   ostr << "(A " << _v << ").(" << _op << ")";
  797. }
  798.  
  799. void Exists::printFormula(ostream & ostr) const
  800. {
  801.   ostr << "(E " << _v << ").(" << _op << ")";
  802. }
  803.  
  804.  
  805. ostream & operator << (ostream & ostr, const Term & t)
  806. {
  807.   t->printTerm(ostr);
  808.   return ostr;
  809. }
  810.  
  811. ostream & operator << (ostream & ostr, const Formula & f)
  812. {
  813.   f->printFormula(ostr);
  814.   return ostr;
  815. }
  816.  
  817.  
  818. // ---------------------------------------------------------------------
  819.  
  820.  
  821. // Funkcije za izracunvanje interpretacija -----------------------------
  822.  
  823. unsigned VariableTerm::eval(const Structure & st, const Valuation & val) const
  824. {
  825.   return val.getValue(_v);
  826. }
  827.  
  828. unsigned FunctionTerm::eval(const Structure & st, const Valuation & val) const
  829. {
  830.   Function * f = st.getFunction(_f);
  831.  
  832.   vector<unsigned> args;
  833.  
  834.   for(unsigned i = 0; i < _ops.size(); i++)
  835.     args.push_back(_ops[i]->eval(st, val));
  836.  
  837.   return f->eval(args);
  838. }  
  839.  
  840. bool True::eval(const Structure & st,
  841.         const Valuation & val) const
  842. {
  843.   return true;
  844. }
  845.  
  846. bool False::eval(const Structure & st,
  847.          const Valuation & val) const
  848. {
  849.   return false;
  850. }
  851.  
  852. bool Atom::eval(const Structure & st,
  853.         const Valuation & val) const
  854. {
  855.   Relation * r = st.getRelation(_p);
  856.  
  857.   vector<unsigned> args;
  858.  
  859.   for(unsigned i = 0; i < _ops.size(); i++)
  860.     args.push_back(_ops[i]->eval(st, val));
  861.  
  862.   return r->eval(args);
  863. }
  864.  
  865. bool Not::eval(const Structure & st,
  866.            const Valuation & val) const
  867. {
  868.   return !_op->eval(st, val);
  869. }
  870.  
  871. bool And::eval(const Structure & st,
  872.            const Valuation & val) const
  873. {
  874.   return _op1->eval(st, val) && _op2->eval(st, val);
  875. }
  876.  
  877.  
  878. bool Or::eval(const Structure & st,
  879.           const Valuation & val) const
  880. {
  881.   return _op1->eval(st, val) || _op2->eval(st, val);
  882. }
  883.  
  884. bool Imp::eval(const Structure & st,
  885.             const Valuation & val) const
  886. {
  887.   return !_op1->eval(st, val) || _op2->eval(st, val);
  888. }
  889.  
  890. bool Iff::eval(const Structure & st,
  891.            const Valuation & val) const
  892. {
  893.   return _op1->eval(st, val) == _op2->eval(st, val);
  894. }
  895.  
  896. bool Forall::eval(const Structure & st,
  897.           const Valuation & val) const
  898. {
  899.   Valuation val_p = val;
  900.   for(unsigned i = 0; i < st.getDomain().size(); i++)
  901.     {
  902.       val_p.setValue(_v, st.getDomain()[i]);
  903.       if(_op->eval(st, val_p) == false)
  904.     return false;
  905.     }
  906.   return true;
  907. }
  908.  
  909.  
  910. bool Exists::eval(const Structure & st,
  911.           const Valuation & val) const
  912. {
  913.   Valuation val_p = val;
  914.   for(unsigned i = 0; i < st.getDomain().size(); i++)
  915.     {
  916.       val_p.setValue(_v, st.getDomain()[i]);
  917.       if(_op->eval(st, val_p) == true)
  918.     return true;
  919.     }
  920.   return false;
  921. }
  922.  
  923. // -----------------------------------------------------------------------
  924.  
  925. // Ostale funkcije clanice -----------------------------------------------
  926.  
  927. // Klasa Signature -------------------------------------------------------
  928.  
  929. void Signature::addFunctionSymbol(const FunctionSymbol & f, unsigned arity)
  930. {
  931.   _functions.insert(make_pair(f, arity));
  932. }
  933.  
  934. void Signature::addPredicateSymbol(const PredicateSymbol & p, unsigned arity)
  935. {
  936.   _predicates.insert(make_pair(p, arity));
  937. }
  938.  
  939. bool Signature::checkFunctionSymbol(const FunctionSymbol & f,
  940.                     unsigned & arity) const
  941. {
  942.   map<FunctionSymbol, unsigned>::const_iterator it = _functions.find(f);
  943.  
  944.   if(it != _functions.end())
  945.     {
  946.       arity = it->second;
  947.       return true;
  948.     }
  949.   else
  950.     return false;
  951. }
  952.  
  953. bool Signature::checkPredicateSymbol(const PredicateSymbol & f,
  954.                      unsigned & arity) const
  955. {
  956.   map<PredicateSymbol, unsigned>::const_iterator it = _predicates.find(f);
  957.  
  958.   if(it != _predicates.end())
  959.     {
  960.       arity = it->second;
  961.       return true;
  962.     }
  963.   else
  964.     return false;
  965. }
  966.  
  967. // -----------------------------------------------------------------------
  968.  
  969. // Klasa Function --------------------------------------------------------
  970.  
  971. Function::Function(unsigned arity)
  972.   :_arity(arity)
  973. {}
  974.  
  975. unsigned Function::getArity()
  976. {
  977.   return _arity;
  978. }
  979. // ----------------------------------------------------------------------
  980.  
  981. // Klasa Relation -------------------------------------------------------
  982.  
  983. Relation::Relation(unsigned arity)
  984.   :_arity(arity)
  985. {}
  986.  
  987. unsigned Relation::getArity()
  988. {
  989.   return _arity;
  990. }
  991. // ----------------------------------------------------------------------
  992.  
  993. // Klasa Structure ------------------------------------------------------
  994.  
  995. Structure::Structure(const Signature & sig, const Domain & domain)
  996.   :_sig(sig),
  997.    _domain(domain)
  998. {}
  999.  
  1000. const Signature & Structure::getSignature() const
  1001. {
  1002.   return _sig;
  1003. }
  1004.  
  1005. const Domain & Structure::getDomain() const
  1006. {
  1007.   return _domain;
  1008. }
  1009.  
  1010. void Structure::addFunction(const FunctionSymbol & fs, Function * f)
  1011. {
  1012.   unsigned arity;
  1013.   if(!_sig.checkFunctionSymbol(fs, arity) || arity != f->getArity())
  1014.     throw "Function arity mismatch";
  1015.  
  1016.   _funs.insert(make_pair(fs, f));
  1017. }
  1018.  
  1019. Function * Structure::getFunction(const FunctionSymbol & f) const
  1020. {
  1021.   map<FunctionSymbol, Function *>::const_iterator it =
  1022.     _funs.find(f);
  1023.  
  1024.   if(it != _funs.end())
  1025.     {
  1026.       return it->second;
  1027.     }
  1028.   else
  1029.     throw "Function symbol unknown!";
  1030. }
  1031.  
  1032. void Structure::addRelation(const PredicateSymbol & ps, Relation * r)
  1033. {
  1034.   unsigned arity;
  1035.   if(!_sig.checkPredicateSymbol(ps, arity) || arity != r->getArity())
  1036.     throw "Relation arity mismatch";
  1037.  
  1038.   _rels.insert(make_pair(ps, r));
  1039. }
  1040.  
  1041. Relation * Structure::getRelation(const PredicateSymbol & p) const
  1042. {
  1043.   map<PredicateSymbol, Relation *>::const_iterator it =
  1044.     _rels.find(p);
  1045.  
  1046.   if(it != _rels.end())
  1047.     {
  1048.       return it->second;
  1049.     }
  1050.   else
  1051.     throw "Predicate symbol unknown!";
  1052. }
  1053.  
  1054. Structure::~Structure()
  1055. {
  1056.   for(const auto & p : _funs)
  1057.     delete p.second;
  1058.   for(const auto & p : _rels)
  1059.     delete p.second;
  1060. }
  1061.  
  1062. // ----------------------------------------------------------------------
  1063.  
  1064. // Klasa Valuation ------------------------------------------------------
  1065.  
  1066. Valuation::Valuation(const Domain & dom)
  1067.     :_domain(dom)
  1068. {}
  1069.  
  1070. const Domain & Valuation::getDomain() const
  1071. {
  1072.   return _domain;
  1073. }
  1074.  
  1075. void Valuation::setValue(const Variable & v, unsigned value)
  1076. {
  1077.   if(find(_domain.begin(), _domain.end(), value) ==
  1078.      _domain.end())
  1079.     throw "Value not in domain!";
  1080.  
  1081.   _values[v] = value;
  1082. }
  1083.  
  1084. unsigned Valuation::getValue(const Variable & v) const
  1085. {
  1086.   map<Variable, unsigned>::const_iterator it =
  1087.     _values.find(v);
  1088.  
  1089.   if(it != _values.end())
  1090.     return it->second;
  1091.   else
  1092.     throw "Variable unknown!";
  1093. }
  1094.  
  1095. // -----------------------------------------------------------------------
  1096.  
  1097. // Klasa BaseTerm ------------------------------------------------------------
  1098.  
  1099. bool BaseTerm::containsVariable(const Variable & v) const
  1100. {
  1101.   VariableSet vars;
  1102.   getVars(vars);
  1103.   return vars.find(v) != vars.end();
  1104. }
  1105. // -----------------------------------------------------------------------
  1106.  
  1107. // Klasa VariableTerm ----------------------------------------------------
  1108.  
  1109. VariableTerm::VariableTerm(const Variable & v)
  1110.   :_v(v)
  1111. {}
  1112.  
  1113. BaseTerm::Type VariableTerm::getType() const
  1114. {
  1115.   return TT_VARIABLE;
  1116. }
  1117.  
  1118. const Variable & VariableTerm::getVariable() const
  1119. {
  1120.   return _v;
  1121. }
  1122.  
  1123. // -----------------------------------------------------------------------
  1124.  
  1125. // Klasa FunctionTerm ----------------------------------------------------
  1126.  
  1127. FunctionTerm::FunctionTerm(const Signature & s, const FunctionSymbol & f,
  1128.                const vector<Term> & ops)
  1129.   :_sig(s),
  1130.    _f(f),
  1131.    _ops(ops)
  1132. {
  1133.   unsigned arity;
  1134.   if(!_sig.checkFunctionSymbol(_f, arity) || arity != _ops.size())
  1135.     throw "Syntax error!";
  1136. }
  1137.  
  1138. FunctionTerm::FunctionTerm(const Signature & s, const FunctionSymbol & f,
  1139.                vector<Term> && ops)
  1140.   :_sig(s),
  1141.    _f(f),
  1142.    _ops(std::move(ops))
  1143. {
  1144.   unsigned arity;
  1145.   if(!_sig.checkFunctionSymbol(_f, arity) || arity != _ops.size())
  1146.     throw "Syntax error!";
  1147. }
  1148.  
  1149.  
  1150. BaseTerm::Type FunctionTerm::getType() const
  1151. {
  1152.   return TT_FUNCTION;
  1153. }
  1154.  
  1155.  
  1156. const Signature & FunctionTerm::getSignature() const
  1157. {
  1158.   return _sig;
  1159. }
  1160.  
  1161. const FunctionSymbol & FunctionTerm::getSymbol() const
  1162. {
  1163.   return _f;
  1164. }
  1165.  
  1166. const vector<Term> & FunctionTerm::getOperands() const
  1167. {
  1168.   return _ops;
  1169. }
  1170.  
  1171. // ----------------------------------------------------------------------
  1172.  
  1173. // Klasa BaseFormula --------------------------------------------------------
  1174.  
  1175. bool BaseFormula::containsVariable(const Variable & v, bool free) const
  1176. {
  1177.   VariableSet vars;
  1178.   getVars(vars, free);
  1179.   return vars.find(v) != vars.end();
  1180. }
  1181.  
  1182. // ----------------------------------------------------------------------
  1183.  
  1184. Variable getUniqueVariable(const Formula & f, const Term & t)
  1185. {
  1186.   static unsigned i = 0;
  1187.  
  1188.   Variable v;
  1189.  
  1190.   do {    
  1191.     v = string("uv") + to_string(++i);
  1192.   } while(t->containsVariable(v) || f->containsVariable(v));
  1193.  
  1194.   return v;
  1195. }
  1196.  
  1197. // ----------------------------------------------------------------------
  1198.  
  1199. // Klasa AtomicFormula --------------------------------------------------
  1200.  
  1201. // Klasa LogicConstant --------------------------------------------------
  1202.  
  1203. BaseFormula::Type True::getType() const
  1204. {
  1205.   return T_TRUE;
  1206. }
  1207. // ----------------------------------------------------------------------
  1208.  
  1209. // Klasa False ----------------------------------------------------------
  1210.  
  1211. BaseFormula::Type False::getType() const
  1212. {
  1213.   return T_FALSE;
  1214. }
  1215.  
  1216. // ----------------------------------------------------------------------
  1217.  
  1218. // Klasa Atom -----------------------------------------------------------
  1219.  
  1220. Atom::Atom(const Signature & s,
  1221.        const PredicateSymbol & p,
  1222.        const vector<Term> & ops)
  1223.   :_sig(s),
  1224.    _p(p),
  1225.    _ops(ops)
  1226. {
  1227.   unsigned arity;
  1228.   if(!_sig.checkPredicateSymbol(_p, arity) || arity != _ops.size())
  1229.     throw "Syntax error!";
  1230. }
  1231.  
  1232. Atom::Atom(const Signature & s,
  1233.        const PredicateSymbol & p,
  1234.        vector<Term> && ops)
  1235.   :_sig(s),
  1236.    _p(p),
  1237.    _ops(std::move(ops))
  1238. {
  1239.   unsigned arity;
  1240.   if(!_sig.checkPredicateSymbol(_p, arity) || arity != _ops.size())
  1241.     throw "Syntax error!";
  1242. }
  1243.  
  1244. const PredicateSymbol & Atom::getSymbol() const
  1245. {
  1246.   return _p;
  1247. }
  1248.  
  1249. const Signature & Atom::getSignature() const
  1250. {
  1251.   return _sig;
  1252. }
  1253.  
  1254. const vector<Term> & Atom::getOperands() const
  1255. {
  1256.   return _ops;
  1257. }
  1258.  
  1259.  
  1260. BaseFormula::Type Atom::getType() const
  1261. {
  1262.   return T_ATOM;
  1263. }
  1264.  
  1265. // -----------------------------------------------------------------------
  1266.  
  1267. // Klasa UnaryConnective -------------------------------------------------
  1268.  
  1269. UnaryConnective::UnaryConnective(const Formula & op)
  1270.   :_op(op)
  1271. {}
  1272.  
  1273. const Formula & UnaryConnective::getOperand() const
  1274. {
  1275.   return _op;
  1276. }
  1277.  
  1278. // -----------------------------------------------------------------------
  1279.  
  1280. // Klasa Not -------------------------------------------------------------
  1281.  
  1282. BaseFormula::Type Not::getType() const
  1283. {
  1284.   return T_NOT;
  1285. }
  1286.  
  1287. // -----------------------------------------------------------------------
  1288.  
  1289. // Klasa BinaryConnective ------------------------------------------------
  1290.  
  1291. BinaryConnective::BinaryConnective( const Formula & op1,  const Formula & op2)
  1292.   :_op1(op1),
  1293.    _op2(op2)
  1294. {}
  1295.  
  1296. const Formula & BinaryConnective::getOperand1() const
  1297. {
  1298.   return _op1;
  1299.   }
  1300.  
  1301. const Formula & BinaryConnective::getOperand2() const
  1302. {
  1303.   return _op2;
  1304. }
  1305.  
  1306.  
  1307. // Klasa And ---------------------------------------------------------------
  1308.  
  1309. BaseFormula::Type And::getType() const
  1310. {
  1311.   return T_AND;
  1312. }
  1313.  
  1314. // -------------------------------------------------------------------------
  1315.  
  1316. // Klasa Or ----------------------------------------------------------------
  1317.  
  1318. BaseFormula::Type Or::getType() const
  1319. {
  1320.   return T_OR;
  1321. }
  1322.  
  1323. // -------------------------------------------------------------------------
  1324.  
  1325. // Klasa Imp ---------------------------------------------------------------
  1326.  
  1327. BaseFormula::Type Imp::getType() const
  1328. {
  1329.   return T_IMP;
  1330. }
  1331.  
  1332. // -------------------------------------------------------------------------
  1333.  
  1334. // Klasa Iff ---------------------------------------------------------------
  1335.  
  1336. BaseFormula::Type Iff::getType() const
  1337. {
  1338.   return T_IFF;
  1339. }
  1340.  
  1341. // -------------------------------------------------------------------------
  1342.  
  1343. // Klasa Quantifier --------------------------------------------------------
  1344.  
  1345. Quantifier::Quantifier(const Variable & v, const Formula & op)
  1346.   :_v(v),
  1347.    _op(op)
  1348. {}
  1349.  
  1350. const Variable & Quantifier::getVariable() const
  1351. {
  1352.   return _v;
  1353. }
  1354.  
  1355. const Formula & Quantifier::getOperand() const
  1356. {
  1357.   return _op;
  1358. }
  1359.  
  1360. // ------------------------------------------------------------------------
  1361.  
  1362. // Klasa Forall -----------------------------------------------------------
  1363.  
  1364. BaseFormula::Type Forall::getType() const
  1365. {
  1366.   return T_FORALL;
  1367. }
  1368.  
  1369. // ------------------------------------------------------------------------
  1370.  
  1371. // Klasa Exists -----------------------------------------------------------
  1372.  
  1373. BaseFormula::Type Exists::getType() const
  1374. {
  1375.   return T_EXISTS;
  1376. }
  1377.  
  1378. // -----------------------------------------------------------------------
  1379. // -----------------------------------------------------------------------
  1380.  
  1381. // Konkretna interpretacija ----------------------------------------------
  1382.  
  1383. /* Klasa predstavlja funkciju-konstantu 0 */
  1384. class Zero : public Function {
  1385.  
  1386. public:
  1387.   Zero()
  1388.     : Function(0)
  1389.   {}
  1390.  
  1391.   virtual unsigned eval(const vector<unsigned> & args)
  1392.   {
  1393.     if(args.size() > 0)
  1394.       throw "Arguments number mismatch";
  1395.  
  1396.     return 0;
  1397.   }
  1398. };
  1399.  
  1400. /* Klasa predstavlja funkciju-konstantu 1 */
  1401. class One : public Function {
  1402.  
  1403. public:
  1404.   One()
  1405.     : Function(0)
  1406.   {}
  1407.  
  1408.   virtual unsigned eval(const vector<unsigned> & args)
  1409.   {
  1410.     if(args.size() > 0)
  1411.       throw "Arguments number mismatch";
  1412.  
  1413.     return 1;
  1414.   }
  1415. };
  1416.  
  1417. /* Klasa predstavlja binarnu funkciju sabiranja po modulu n */
  1418. class Plus : public Function {
  1419. private:
  1420.   unsigned _domain_size;
  1421. public:
  1422.   Plus(unsigned domain_size)
  1423.     : Function(2),
  1424.       _domain_size(domain_size)
  1425.   {}
  1426.  
  1427.   virtual unsigned eval(const vector<unsigned> & args)
  1428.   {
  1429.     if(args.size() != 2)
  1430.       throw "Arguments number mismatch";
  1431.    
  1432.     return (args[0] + args[1]) % _domain_size;
  1433.   }
  1434.  
  1435. };
  1436.  
  1437. /* Klasa predstavlja binarnu funkciju mnozenja po modulu n */
  1438. class Times : public Function {
  1439. private:
  1440.   unsigned _domain_size;
  1441. public:
  1442.   Times(unsigned domain_size)
  1443.     : Function(2),
  1444.       _domain_size(domain_size)
  1445.   {}
  1446.  
  1447.   virtual unsigned eval(const vector<unsigned> & args)
  1448.   {
  1449.     if(args.size() != 2)
  1450.       throw "Arguments number mismatch";
  1451.    
  1452.     return (args[0] * args[1]) % _domain_size;
  1453.   }
  1454.  
  1455. };
  1456.  
  1457. /* Klasa predstavlja unarnu relaciju koja sadrzi sve parne brojeve */
  1458. class Even : public Relation {
  1459.  
  1460. public:
  1461.   Even()
  1462.     : Relation(1)
  1463.   {}
  1464.  
  1465.   virtual bool eval(const vector<unsigned> & args)
  1466.   {
  1467.     if(args.size() != 1)
  1468.       throw "Arguments number mismatch";
  1469.    
  1470.     return args[0] % 2 == 0;
  1471.   }
  1472.  
  1473. };
  1474.  
  1475. /* Klasa predstavlja unarnu relaciju koja sadrzi sve neparne brojeve */
  1476. class Odd : public Relation {
  1477.  
  1478. public:
  1479.   Odd()
  1480.     : Relation(1)
  1481.   {}
  1482.  
  1483.   virtual bool eval(const vector<unsigned> & args)
  1484.   {
  1485.     if(args.size() != 1)
  1486.       throw "Arguments number mismatch";
  1487.    
  1488.     return args[0] % 2 == 1;
  1489.   }
  1490.  
  1491. };
  1492.  
  1493. /* Klasa predstavlja binarnu relaciju jednakosti */
  1494. class Equal : public Relation {
  1495.  
  1496. public:
  1497.   Equal()
  1498.     : Relation(2)
  1499.   {}
  1500.  
  1501.   virtual bool eval(const vector<unsigned> & args)
  1502.   {
  1503.     if(args.size() != 2)
  1504.       throw "Arguments number mismatch";
  1505.    
  1506.     return args[0] == args[1];
  1507.   }
  1508.  
  1509. };
  1510.  
  1511. /* Klasa predstavlja binarnu relaciju manje ili jednako */
  1512. class LowerOrEqual : public Relation {
  1513.  
  1514. public:
  1515.   LowerOrEqual()
  1516.     : Relation(2)
  1517.   {}
  1518.  
  1519.   virtual bool eval(const vector<unsigned> & args)
  1520.   {
  1521.     if(args.size() != 2)
  1522.       throw "Arguments number mismatch";
  1523.    
  1524.     return args[0] <= args[1];
  1525.   }
  1526.  
  1527. };
  1528.  
  1529. /* Test program */
  1530. int main()
  1531. {
  1532.  
  1533.   /* Definisemo strukturu */
  1534.   Signature s;
  1535.  
  1536.   /* Dodajemo funkcijske i predikatske simbole */
  1537.   s.addFunctionSymbol("0", 0);
  1538.   s.addFunctionSymbol("1", 0);
  1539.   s.addFunctionSymbol("+", 2);
  1540.   s.addFunctionSymbol("*", 2);
  1541.   s.addPredicateSymbol("even", 1);
  1542.   s.addPredicateSymbol("odd", 1);
  1543.   s.addPredicateSymbol("=", 2);
  1544.   s.addPredicateSymbol("<=", 2);
  1545.  
  1546.  
  1547.   /* Primeri termova i formula */
  1548.  
  1549.   Term t0 = make_shared<FunctionTerm>(s, "0");
  1550.   Term t1 = make_shared<FunctionTerm>(s, "1");
  1551.  
  1552.   Formula f0 = make_shared<Atom>(s, "even", vector<Term> { t0 });
  1553.  
  1554.   cout << f0 << endl;
  1555.  
  1556.   Formula f1 = make_shared<Atom>(s, "even", vector<Term> { t1 });
  1557.  
  1558.   cout << f1 << endl;
  1559.  
  1560.   Term tx = make_shared<VariableTerm>("x");
  1561.   Term ty = make_shared<VariableTerm>("y");
  1562.    
  1563.   Term xpy = make_shared<FunctionTerm>(s, "+", vector<Term> {tx, ty});
  1564.  
  1565.   Formula xeven = make_shared<Atom>(s, "even", vector<Term> { tx });
  1566.  
  1567.   Formula yeven = make_shared<Atom>(s, "even", vector<Term> { ty });
  1568.  
  1569.   Formula xpyeven = make_shared<Atom>(s, "even", vector<Term> { xpy });
  1570.  
  1571.   cout << xpyeven << endl;
  1572.  
  1573.   Formula xandy = make_shared<And>(xeven, yeven);
  1574.   Formula imp = make_shared<Imp>(xandy, xpyeven);
  1575.  
  1576.   Formula forall_x = make_shared<Forall>("x", imp);
  1577.   Formula forall_y = make_shared<Forall>("y", forall_x);
  1578.  
  1579.   cout << forall_y << endl;
  1580.  
  1581.   /* Semantika */
  1582.  
  1583.   /* Definisemo domen D = {0, 1, 2, ..., n-1 } */
  1584.  
  1585.   Domain domain;
  1586.   for(unsigned i = 0; i < 8; i++)
  1587.     domain.push_back(i);
  1588.  
  1589.  
  1590.   /* Definisemo L-strukturu */
  1591.   Structure st(s, domain);
  1592.  
  1593.   /* Dodeljujemo interpretacije simbolima iz signature */
  1594.   st.addFunction("0", new Zero());
  1595.   st.addFunction("1", new One());
  1596.   st.addFunction("+", new Plus(domain.size()));
  1597.   st.addFunction("*", new Times(domain.size()));
  1598.   st.addRelation("even", new Even());  
  1599.   st.addRelation("odd", new Odd());  
  1600.   st.addRelation("=", new Equal());  
  1601.   st.addRelation("<=", new LowerOrEqual());  
  1602.  
  1603.   /* Definisemo valuaciju */
  1604.   Valuation val(domain);
  1605.   val.setValue("x", 1);
  1606.   val.setValue("y", 3);
  1607.  
  1608.   /* Primeri izracunavanja vrednosti termova i formula */
  1609.   cout << xpy->eval(st, val) << endl;
  1610.  
  1611.   cout << forall_y->eval(st,val) << endl;
  1612.  
  1613.   Formula and_f = make_shared<And>(xeven, forall_y);
  1614.  
  1615.   cout << and_f << endl;
  1616.  
  1617.   cout << and_f->eval(st, val) << endl;
  1618.  
  1619.   return 0;
  1620. }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!