summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--main.cpp37
-rw-r--r--tree.cpp46
-rw-r--r--tree.h12
3 files changed, 83 insertions, 12 deletions
diff --git a/main.cpp b/main.cpp
index 2b7e748..f4fe639 100644
--- a/main.cpp
+++ b/main.cpp
@@ -42,9 +42,8 @@ vector<Axiom> importAxioms(const vector<string> &list){
using Heuristic = int (*)(const Tree&);
-int heuristic(const Tree &tree){
- return tree.nleaves();
-}
+int heuristic_nleaves(const Tree &tree){return tree.nleaves();}
+int heuristic_height(const Tree &tree){return tree.height();}
template <Heuristic F>
struct AscendingCompare{
@@ -99,25 +98,43 @@ vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const T
}
+void test_func(){
+ Tree from("([2]*([2]*1))"),to("10");
+ Tree subj("(([1]*1)*[1])");
+
+ /*unordered_set<Variable> temps=to.collectTemporaries();
+ for(Variable v : temps){
+ cout<<v<<endl;
+ }*/
+
+ vector<Tree> res=subj.replace(from,to);
+ for(const Tree &t : res){
+ cout<<t<<endl;
+ }
+}
+
int main(){
+ test_func();
+ return 0;
+
const vector<Axiom> axioms=importAxioms({
- // "([1]*[2])>([2]*[1])",
- // "(([1]*[2])*[3])=([1]*([2]*[3]))",
+ // "([1]*[2])>([2]*[1])", // Commutativity
+ // "(([1]*[2])*[3])=([1]*([2]*[3]))", // Associativity
- // "([1]*([1]*[2]))=[1]",
- // "(([2]*[1])*[1])=[1]",
+ "([1]*([1]*[2]))=[1]", // Onno's 1=2 axioms
+ "(([2]*[1])*[1])=[1]",
// "[1]=([1]*[1])",
// "(([1]*[2])*[3])=(([2]*[3])*[1])",
- "[1]=[2]",
+ // "[1]=[2]",
});
- const Tree t_from("(1*2)"),t_to("(2*1)");
+ const Tree t_from("1"),t_to("2");
for(const Axiom &ax : axioms)cout<<ax<<endl;
cout<<endl;
- vector<Tree> *res=deduceEq<heuristic>(axioms,t_from,t_to);
+ vector<Tree> *res=deduceEq<heuristic_nleaves>(axioms,t_from,t_to);
if(res==nullptr){
cout<<"No deduction"<<endl;
} else {
diff --git a/tree.cpp b/tree.cpp
index 8d677db..a259e9b 100644
--- a/tree.cpp
+++ b/tree.cpp
@@ -11,6 +11,8 @@ int uniqid(){
}
+Variable::Variable(int id):id(id){}
+
bool Variable::isOperator() const {
return id==0;
}
@@ -167,6 +169,15 @@ Tree::Node* Tree::Node::apply(const Assign &as) const {
return n;
}
+void Tree::Node::collectTemporaries(unordered_set<Variable> &accum) const {
+ if(v.isOperator()){
+ left->collectTemporaries(accum);
+ right->collectTemporaries(accum);
+ } else {
+ accum.insert(v);
+ }
+}
+
int Tree::Node::nleaves() const {
if(v.isOperator()){
return left->nleaves()+right->nleaves();
@@ -175,6 +186,11 @@ int Tree::Node::nleaves() const {
}
}
+int Tree::Node::height() const {
+ if(v.isOperator())return max(left->height(),right->height());
+ else return 1;
+}
+
int Tree::Node::compare(const Node &other) const {
if(v.isTemp()&&other.v.isTemp())return 0;
if(v<other.v)return -1;
@@ -283,9 +299,27 @@ bool Tree::matches(const Tree &pat) const {
}
}
+void Tree::refreshUnassigned(const Tree &repl,Assign &as) const {
+ unordered_set<Variable> temps=repl.collectTemporaries();
+ // cerr<<"rU:"<<endl;
+ for(Variable v : temps){
+ // cerr<<" v = "<<v<<endl;
+ if(v.isTemp()&&as.find(v)==as.end()){
+ int id=uniqid();
+ as.emplace(v,Node(id));
+ // cerr<<" emplace("<<v<<","<<Node(id)<<")"<<endl;
+ }
+ }
+}
+
void Tree::replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum){
Assign *as=subj->match(*pat.root);
if(as){
+ refreshUnassigned(repl,*as);
+ cerr<<"replace("<<*subj<<","<<pat<<","<<repl<<"); as:"<<endl;
+ for(const pair<Variable,Node> &p : *as){
+ cerr<<" "<<p.first<<" -> "<<p.second<<endl;
+ }
Node *res=repl.root->apply(*as);
Node backup=*subj;
*subj=*res;
@@ -307,11 +341,23 @@ vector<Tree> Tree::replace(const Tree &pat,const Tree &repl){
return res;
}
+unordered_set<Variable> Tree::collectTemporaries() const {
+ assert(root);
+ unordered_set<Variable> temps;
+ root->collectTemporaries(temps);
+ return temps;
+}
+
int Tree::nleaves() const {
assert(root);
return root->nleaves();
}
+int Tree::height() const {
+ assert(root);
+ return root->height();
+}
+
int Tree::compare(const Tree &other) const {
assert(root&&other.root);
return root->compare(*other.root);
diff --git a/tree.h b/tree.h
index 7d8cf15..5f008d7 100644
--- a/tree.h
+++ b/tree.h
@@ -4,6 +4,7 @@
#include <string>
#include <vector>
#include <unordered_map>
+#include <unordered_set>
using namespace std;
@@ -13,7 +14,7 @@ int uniqid();
struct Variable{
int id;
- Variable(int id):id(id){}
+ Variable(int id);
bool isOperator() const;
bool isFixed() const;
@@ -25,6 +26,8 @@ struct Variable{
operator int() const;
};
+ostream& operator<<(ostream &os,const Variable &v);
+
namespace std {
template <>
struct hash<Variable>{
@@ -50,10 +53,11 @@ class Tree{
Node& operator=(const Node &other);
Assign* match(const Node &pat,Assign *accum=nullptr) const;
-
Node* apply(const Assign &as) const;
+ void collectTemporaries(unordered_set<Variable> &accum) const;
int nleaves() const;
+ int height() const;
int compare(const Node &other) const;
};
@@ -65,6 +69,8 @@ class Tree{
void replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum);
+ void refreshUnassigned(const Tree &repl,Assign &as) const;
+
public:
Tree(); // Creates invalid tree
Tree(const string &expr);
@@ -75,8 +81,10 @@ public:
bool matches(const Tree &pat) const;
vector<Tree> replace(const Tree &pat,const Tree &repl);
+ unordered_set<Variable> collectTemporaries() const;
int nleaves() const;
+ int height() const;
int compare(const Tree &other) const;